Commit 2022-07-08 02:55 0e3184fc
View on Github →feat(data/fin/tuple/basic): add lemmas for rewriting exists and forall over n+1-tuples (#15048)
The lemma names fin.forall_fin_succ_pi and fin.exists_fin_succ_pi mirror the existing fin.forall_fin_succ and fin.exists_fin_succ.