English
Equality predicates on a type are determined by their pointwise values: if two BEq structures agree on all pairs x,y, then the two BEq structures are identical.
Русский
Предикаты равенства на заданном множестве определяются по их значению на паре элементов: если две структуры BEq совпадают на всех парах x,y, то эти структуры совпадают.
LaTeX
$$$ \forall (inst1 inst2 : BEq \alpha),\ (\forall x,y,\ @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) \Rightarrow inst1 = inst2 $$$
Lean4
@[ext]
theorem beq_ext {α : Type*} (inst1 : BEq α) (inst2 : BEq α) (h : ∀ x y, @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) :
inst1 = inst2 := by
have ⟨beq1⟩ := inst1
congr
funext x y
exact h x y
