Commit 2024-10-04 14:05 2ae9a800

View on Github →

feat: a = cast e b ↔ HEq a b (#17294) From LeanCamCombi

Estimated changes

Modified Mathlib/Logic/Basic.lean

added theorem eq_cast_iff_heq

added theorem heq_of_eq_cast