Theorem cast_heq_iff_heq

Modification history

2025-01-21 00:20
Mathlib/Logic/Basic.lean
feat(Logic/Basic): `HEq (cast h a) b ↔ HEq a b` (#20847) …
Added cast_heq_iff_heqView on Github →