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 HUne: U ≠ Empty.
An exact proof term for the current goal is (andER (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty)) (U ≠ Empty) H2).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty)) (V ≠ Empty) H1).
Apply andI to the current goal.
An exact proof term for the current goal is (nonempty_has_element U HUne).
An exact proof term for the current goal is (nonempty_has_element V HVne).
∎