Let y and z be given.
We will prove y ∈ {y,z}.
rewrite the current goal using (If_i_1 (Empty ∈ 𝒫 Empty) y z (Empty_In_Power 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 (Self_In_Power (𝒫 Empty)).
∎