We will prove (∀u ∈ An, f u ∈ ordsucc n) ∧ (∀u v ∈ An, f u = f v → u = v).

Apply andI to the current goal.

Let u be given.

Assume Hu: u ∈ An.

An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ f a0 ∈ ordsucc n) u Hu).

Let u be given.

Assume Hu: u ∈ An.

Let v be given.

Assume Hv: v ∈ An.

Assume Heq: f u = f v.

We prove the intermediate claim HuA: u ∈ A.

An exact proof term for the current goal is (SepE1 A (λa0 : set ⇒ f a0 ∈ ordsucc n) u Hu).

We prove the intermediate claim HvA: v ∈ A.

An exact proof term for the current goal is (SepE1 A (λa0 : set ⇒ f a0 ∈ ordsucc n) v Hv).

We prove the intermediate claim Hinj0: ∀x z ∈ A, f x = f z → x = z.

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

An exact proof term for the current goal is (Hinj0 u HuA v HvA Heq).