theorem ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x ↦ propext (h x))事実 半形式的：
$`\text{Fact ext}\\
\text{For } a, b : \mathrm{Set}\: \alpha \\
\text{When } \forall (x : α),\, x \in a \iff x \in b \\
\text{Holds }a = b
`$
事実 シーケント：
$`\text{ext} := \big( (a, b : \mathrm{Set}(\alpha) ), (\forall (x : α),\, x \in a \iff x \in b) \vdash!\; a = b \big)`$
