Let P of type prop be given.
Set p1 to be the term λx : set ⇒ x = Empty ∨ P.
Set p2 to be the term λx : set ⇒ x ≠ Empty ∨ P.
We prove the intermediate claim L1: p1 Empty.
We will prove (Empty = Empty ∨ P).
Apply orIL to the current goal.
An exact proof term for the current goal is (λq H ⇒ H).
We prove the intermediate claim L2: (Eps_i p1) = Empty ∨ P.
An exact proof term for the current goal is (Eps_i_ax p1 Empty L1).
We prove the intermediate claim L3: p2 (𝒫 Empty).
We will prove ¬ (𝒫 Empty = Empty) ∨ P.
Apply orIL to the current goal.
Assume H1: 𝒫 Empty = Empty.
Apply EmptyE Empty to the current goal.
We will prove Empty ∈ Empty.
rewrite the current goal using H1 (from right to left) at position 2.
Apply Empty_In_Power to the current goal.
We prove the intermediate claim L4: Eps_i p2 ≠ Empty ∨ P.
An exact proof term for the current goal is (Eps_i_ax p2 (𝒫 Empty) L3).
Apply L2 to the current goal.
Assume H1: Eps_i p1 = Empty.
Apply L4 to the current goal.
Assume H2: Eps_i p2 ≠ Empty.
We will prove P ∨ ¬ P.
Apply orIR to the current goal.
We will prove ¬ P.
Assume H3: P.
We prove the intermediate claim L5: p1 = p2.
Apply pred_ext to the current goal.
Let x be given.
Apply iffI to the current goal.
Assume H4.
We will prove (¬ (x = Empty) ∨ P).
Apply orIR to the current goal.
We will prove P.
An exact proof term for the current goal is H3.
Assume H4.
We will prove (x = Empty ∨ P).
Apply orIR to the current goal.
We will prove P.
An exact proof term for the current goal is H3.
Apply H2 to the current goal.
rewrite the current goal using L5 (from right to left).
An exact proof term for the current goal is H1.
Assume H2: P.
We will prove P ∨ ¬ P.
Apply orIL to the current goal.
We will prove P.
An exact proof term for the current goal is H2.
Assume H1: P.
We will prove P ∨ ¬ P.
Apply orIL to the current goal.
We will prove P.
An exact proof term for the current goal is H1.
∎