Commit 2023-02-28 15:58 39c00cb1

View on Github →

feat: forward port Mathlib.Logic.Basic lemmas (#2515) logic.basic@feb99064803fd3108e37c18b0f77d0a8344677a3..13cd3e89b30352d5b1b7349f5537ea18ba878e40

Estimated changes

Modified Mathlib/Logic/Basic.lean

added theorem heq_rec_iff_heq

added theorem rec_heq_iff_heq