Let y and z be given.
We will prove z ∈ {y,z}.
rewrite the current goal using (If_i_0 (Empty ∈ Empty) y z (EmptyE Empty)) (from right to left) at position 1.
We will prove (if Empty ∈ Empty then y else z) ∈ {y,z}.
We will prove (if Empty ∈ Empty then y else z) ∈ {if Empty ∈ X then y else z|X ∈ 𝒫 (𝒫 Empty)}.
Apply (ReplI (𝒫 (𝒫 Empty)) (λX : set ⇒ if (Empty ∈ X) then y else z) Empty) to the current goal.
We will prove Empty ∈ 𝒫 (𝒫 Empty).
An exact proof term for the current goal is (Empty_In_Power (𝒫 Empty)).
∎