English
If p and q are pointwise equivalent (p x ↔ q x for all x), then a heterogeneous equality between subtypes a1 : Subtype p and a2 : Subtype q is equivalent to equality of their underlying elements.
Русский
Если подстановки p и q совпадают на каждом элементе (p x ↔ q x для всех x), то гетерогенная эквивалентность подтипов a1 : Subtype p и a2 : Subtype q эквивалентна равенству их базовых значений.
LaTeX
$$$$ (a_1 \;\text{HEq} \; a_2) \iff (a_1 : \alpha) = (a_2 : \alpha) $$ при предположении $\forall x, p(x) \leftrightarrow q(x)$.$$
Lean4
theorem coe_eq_iff {a : { a // p a }} {b : α} : ↑a = b ↔ ∃ h, a = ⟨b, h⟩ := by grind
