Let X, Y and f be given.

Assume Hinj: inj X Y f.

We will prove equip X {f x|x ∈ X}.

We will prove ∃g : set → set, bij X {f x|x ∈ X} g.

We use f to witness the existential quantifier.

We will prove bij X {f x|x ∈ X} f.

We will prove ((∀u ∈ X, f u ∈ {f x|x ∈ X}) ∧ (∀u v ∈ X, f u = f v → u = v)) ∧ (∀w ∈ {f x|x ∈ X}, ∃u ∈ X, f u = w).

Apply andI to the current goal.

Let u be given.

Assume Hu: u ∈ X.

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ f x0) u Hu).

An exact proof term for the current goal is (andER (∀x ∈ X, f x ∈ Y) (∀x z ∈ X, f x = f z → x = z) Hinj).

Let w be given.

Assume Hw: w ∈ {f x|x ∈ X}.

We will prove ∃u ∈ X, f u = w.

Apply (ReplE_impred X (λx0 : set ⇒ f x0) w Hw (∃u ∈ X, f u = w)) to the current goal.

Let u be given.

Assume HuX: u ∈ X.

Assume Hweq: w = f u.

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HuX.

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

Use reflexivity.

∎