Let X and f be given.

Assume H1.

Let x be given.

Assume Hx.

We prove the intermediate claim L1: inv X f (f x) ∈ X ∧ f (inv X f (f x)) = f x.

Apply Eps_i_ax (λx' ⇒ x' ∈ X ∧ f x' = f x) x to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

Use reflexivity.

Apply L1 to the current goal.

Assume H2 H3.

An exact proof term for the current goal is H1 (inv X f (f x)) H2 x Hx H3.

∎