Theorem heq_of_eq_cast

Modification history

2024-10-04 14:05
Mathlib/Logic/Basic.lean
feat: `a = cast e b ↔ HEq a b` (#17294) …
Added heq_of_eq_castView on Github →