Let α and x be given.
Assume Ha Hx.
Apply Hx to the current goal.
Assume Hx1: x ⊆ SNoElts_ α.
Assume Hx2: ∀β ∈ α, exactly1of2 (β ' ∈ x) (β ∈ x).
Apply set_ext to the current goal.
We will prove x ⊆ PSNo α (λβ ⇒ β ∈ x).
Let u be given.
Assume Hu: u ∈ x.
Apply binunionE α {β '|β ∈ α} u (Hx1 u Hu) to the current goal.
Assume H1: u ∈ α.
We will prove u ∈ {β ∈ α|β ∈ x} ∪ {β '|β ∈ α, β ∉ x}.
Apply binunionI1 to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Hu.
Assume H1: u ∈ {β '|β ∈ α}.
Apply ReplE_impred α (λβ ⇒ β ') u H1 to the current goal.
Let β be given.
Assume H2: β ∈ α.
Assume H3: u = β '.
We will prove u ∈ {β ∈ α|β ∈ x} ∪ {β '|β ∈ α, β ∉ x}.
Apply binunionI2 to the current goal.
We will prove u ∈ {β '|β ∈ α, β ∉ x}.
rewrite the current goal using H3 (from left to right).
We will prove β ' ∈ {β '|β ∈ α, β ∉ x}.
We prove the intermediate claim L2: β ∉ x.
Assume H4: β ∈ x.
Apply exactly1of2_E (β ' ∈ x) (β ∈ x) (Hx2 β H2) to the current goal.
Assume H5: β ' ∈ x.
Assume H6: β ∉ x.
An exact proof term for the current goal is H6 H4.
Assume H4: β ' ∉ x.
Assume H5: β ∈ x.
Apply H4 to the current goal.
We will prove (β ') ∈ x.
rewrite the current goal using H3 (from right to left).
We will prove u ∈ x.
An exact proof term for the current goal is Hu.
An exact proof term for the current goal is ReplSepI α (λβ ⇒ β ∉ x) (λβ ⇒ β ') β H2 L2.
We will prove PSNo α (λβ ⇒ β ∈ x) ⊆ x.
Let u be given.
Assume Hu: u ∈ PSNo α (λβ ⇒ β ∈ x).
We will prove u ∈ x.
Apply binunionE {β ∈ α|β ∈ x} {β '|β ∈ α, β ∉ x} u Hu to the current goal.
Assume H1: u ∈ {β ∈ α|β ∈ x}.
Apply SepE α (λβ ⇒ β ∈ x) u H1 to the current goal.
Assume H2: u ∈ α.
Assume H3: u ∈ x.
An exact proof term for the current goal is H3.
Assume H1: u ∈ {β '|β ∈ α, β ∉ x}.
Apply ReplSepE_impred α (λβ ⇒ β ∉ x) (λβ ⇒ β ') u H1 to the current goal.
Let β be given.
Assume H2: β ∈ α.
Assume H3: β ∉ x.
Assume H4: u = β '.
Apply exactly1of2_E (β ' ∈ x) (β ∈ x) (Hx2 β H2) to the current goal.
Assume H5: β ' ∈ x.
Assume H6: β ∉ x.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H5.
Assume H4: β ' ∉ x.
Assume H5: β ∈ x.
We will prove False.
An exact proof term for the current goal is H3 H5.
∎