Let X, Y and f be given.

Assume H1.

Apply H1 to the current goal.

Assume H2.

Apply H2 to the current goal.

Assume H3: ∀u ∈ X, f u ∈ Y.

Assume H4: ∀u v ∈ X, f u = f v → u = v.

Assume H5: ∀w ∈ Y, ∃u ∈ X, f u = w.

Set g to be the term λy ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y) of type set → set.

We prove the intermediate claim L1: ∀y ∈ Y, g y ∈ X ∧ f (g y) = y.

An exact proof term for the current goal is surj_rinv X Y f H5.

We will prove (∀u ∈ Y, g u ∈ X) ∧ (∀u v ∈ Y, g u = g v → u = v) ∧ (∀w ∈ X, ∃u ∈ Y, g u = w).

Apply and3I to the current goal.

We will prove ∀u ∈ Y, g u ∈ X.

Let u be given.

Assume Hu.

Apply L1 u Hu to the current goal.

Assume H _.

An exact proof term for the current goal is H.

We will prove ∀u v ∈ Y, g u = g v → u = v.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv H6.

We will prove u = v.

Apply L1 u Hu to the current goal.

Assume H7: g u ∈ X.

Assume H8: f (g u) = u.

Apply L1 v Hv to the current goal.

Assume H9: g v ∈ X.

Assume H10: f (g v) = v.

rewrite the current goal using H8 (from right to left).

rewrite the current goal using H10 (from right to left).

rewrite the current goal using H6 (from right to left).

Use reflexivity.

We will prove ∀w ∈ X, ∃u ∈ Y, g u = w.

Let w be given.

Assume Hw.

We prove the intermediate claim Lfw: f w ∈ Y.

An exact proof term for the current goal is H3 w Hw.

We use f w to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Lfw.

An exact proof term for the current goal is inj_linv X f H4 w Hw.

∎