Let X, U and V be given.
Assume Hsep.
We prove the intermediate claim H1: (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty.
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) Hsep).
We prove the intermediate claim H2: ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty.
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) H1).
We prove the intermediate claim H3: (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) H2).
We prove the intermediate claim Hleft: U ∈ 𝒫 X ∧ V ∈ 𝒫 X.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) H3).
Apply andI to the current goal.
An exact proof term for the current goal is (PowerE X U (andEL (U ∈ 𝒫 X) (V ∈ 𝒫 X) Hleft)).
An exact proof term for the current goal is (PowerE X V (andER (U ∈ 𝒫 X) (V ∈ 𝒫 X) Hleft)).
∎