Apply nat_complete_ind to the current goal.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, Inj1 m = ordsucc m.

We will prove Inj1 n = ordsucc n.

Apply set_ext to the current goal.

We will prove Inj1 n ⊆ ordsucc n.

Let z be given.

Assume H1: z ∈ Inj1 n.

We will prove z ∈ ordsucc n.

Apply (Inj1E n z H1) to the current goal.

Assume H2: z = 0.

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

We will prove 0 ∈ ordsucc n.

An exact proof term for the current goal is (nat_0_in_ordsucc n Hn).

Assume H2: ∃m ∈ n, z = Inj1 m.

Apply (exandE_i (λm ⇒ m ∈ n) (λm ⇒ z = Inj1 m) H2) to the current goal.

Let m be given.

Assume H3: m ∈ n.

Assume H4: z = Inj1 m.

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

We will prove Inj1 m ∈ ordsucc n.

rewrite the current goal using (IHn m H3) (from left to right).

We will prove ordsucc m ∈ ordsucc n.

An exact proof term for the current goal is (nat_ordsucc_in_ordsucc n Hn m H3).

We will prove ordsucc n ⊆ Inj1 n.

Let m be given.

Assume H1: m ∈ ordsucc n.

We will prove m ∈ Inj1 n.

Apply (ordsuccE n m H1) to the current goal.

Assume H2: m ∈ n.

Apply (nat_inv m (nat_p_trans n Hn m H2)) to the current goal.

Assume H3: m = 0.

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

We will prove 0 ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I1 n).

Assume H3: ∃k, nat_p k ∧ m = ordsucc k.

Apply (exandE_i nat_p (λk ⇒ m = ordsucc k) H3) to the current goal.

Let k be given.

Assume H4: nat_p k.

Assume H5: m = ordsucc k.

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

We will prove ordsucc k ∈ Inj1 n.

We prove the intermediate claim L1: k ∈ m.

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

An exact proof term for the current goal is (ordsuccI2 k).

We prove the intermediate claim L2: k ∈ n.

An exact proof term for the current goal is (nat_trans n Hn m H2 k L1).

rewrite the current goal using (IHn k L2) (from right to left).

We will prove Inj1 k ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I2 n k L2).

Assume H2: m = n.

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

We will prove n ∈ Inj1 n.

Apply (nat_inv n Hn) to the current goal.

Assume H3: n = 0.

rewrite the current goal using H3 (from left to right) at position 1.

We will prove 0 ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I1 n).

Assume H3: ∃k, nat_p k ∧ n = ordsucc k.

Apply (exandE_i nat_p (λk ⇒ n = ordsucc k) H3) to the current goal.

Let k be given.

Assume H4: nat_p k.

Assume H5: n = ordsucc k.

rewrite the current goal using H5 (from left to right) at position 1.

We will prove ordsucc k ∈ Inj1 n.

We prove the intermediate claim L1: k ∈ n.

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

An exact proof term for the current goal is (ordsuccI2 k).

rewrite the current goal using (IHn k L1) (from right to left).

We will prove Inj1 k ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I2 n k L1).