Commit 2023-10-05 11:48 994364d2
View on Github →feat: add lemma List.getD_map (#7307)
Adds a lemma, analogous to Option.getD_map, but for List.
Also fixes a few nearby lemmas to use induction/cases instead of induction'/cases'
~~
feat: add lemma List.getD_map (#7307)
Adds a lemma, analogous to Option.getD_map, but for List.
Also fixes a few nearby lemmas to use induction/cases instead of induction'/cases'
~~