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