Let x, y and z be given.
Assume H1: x ∈ {y,z}.
Apply (ReplE (𝒫 (𝒫 Empty)) (λX ⇒ if Empty ∈ X then y else z) x H1) to the current goal.
Let X be given.
Assume H2: X ∈ 𝒫 (𝒫 Empty) ∧ x = if Empty ∈ X then y else z.
We prove the intermediate claim L1: x = if Empty ∈ X then y else z.
An exact proof term for the current goal is (andER (X ∈ 𝒫 (𝒫 Empty)) (x = if Empty ∈ X then y else z) H2).
Apply (If_i_or (Empty ∈ X) y z) to the current goal.
Assume H3: (if Empty ∈ X then y else z) = y.
Apply orIL to the current goal.
We will prove x = y.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L1.
Assume H3: (if Empty ∈ X then y else z) = z.
Apply orIR to the current goal.
We will prove x = z.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L1.
∎