Theorem heq_cast_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 heq_cast_iff_heqView on Github →