Commit 2024-04-04 16:42 1d5ae615

View on Github →

chore: Remove Init.Propext (#10709) These lemmas can easily go to Logic.Basic

Estimated changes

deleted theorem Iff.to_eq
deleted theorem eq_false_intro
deleted theorem eq_true_intro
deleted theorem iff_eq_eq
deleted theorem imp_congr_ctx_eq
deleted theorem imp_congr_eq
added theorem eq_false_intro
added theorem eq_true_intro
added theorem iff_eq_eq
added theorem imp_congr_ctx_eq
added theorem imp_congr_eq