English
Two Semiquots are equal if and only if their underlying sets s are equal.
Русский
Два Semiquot равны тогда, когда совпадают их основания s.
LaTeX
$$$\forall {q_1 q_2 : Semiquot α},\ q_1 = q_2 \iff q_1.s = q_2.s$$$
Lean4
theorem ext_s {q₁ q₂ : Semiquot α} : q₁ = q₂ ↔ q₁.s = q₂.s :=
by
refine ⟨congr_arg _, fun h => ?_⟩
obtain ⟨_, v₁⟩ := q₁; obtain ⟨_, v₂⟩ := q₂; congr
exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂