Commit 2023-01-07 18:00 44fcc2bf
View on Github →feat: port the basic lemmas in Init.Meta.WellFoundedTactics (#1392) This file contained a few lemmas that should really have gone elsewhere already, before the actual meta code. I'm only porting those in this PR.