Let p, x and y be given.
Apply (xm p) to the current goal.
Assume H1: p.
We prove the intermediate claim L1: p ∧ x = x ∨ ¬ p ∧ x = y.
Apply orIL to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Use reflexivity.
An exact proof term for the current goal is (Eps_i_ax (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y) x L1).
Assume H1: ¬ p.
We prove the intermediate claim L1: p ∧ y = x ∨ ¬ p ∧ y = y.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Use reflexivity.
An exact proof term for the current goal is (Eps_i_ax (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y) y L1).
∎