Apply nat_ind (λn ⇒ ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)) to the current goal.
We will prove ∀f : set → set, (∀i ∈ 1, f i ∈ 0) → ¬ (∀i j ∈ 1, f i = f j → i = j).
Let f be given.
Assume H1.
Apply EmptyE (f 0) (H1 0 In_0_1) to the current goal.
Let n be given.
Assume Hn: nat_p n.
Assume IH: ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j).
Let f be given.
Assume H1: ∀i ∈ ordsucc (ordsucc n), f i ∈ ordsucc n.
Assume H2: ∀i j ∈ ordsucc (ordsucc n), f i = f j → i = j.
Apply xm (∃i ∈ ordsucc (ordsucc n), f i = n) to the current goal.
Assume H3.
Apply H3 to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Assume Hk1: k ∈ ordsucc (ordsucc n).
Assume Hk2: f k = n.
Set f' to be the term λi : set ⇒ if k ⊆ i then f (ordsucc i) else f i.
Apply IH f' to the current goal.
We will prove ∀i ∈ ordsucc n, f' i ∈ n.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Apply xm (k ⊆ i) to the current goal.
Assume H4: k ⊆ i.
We will prove (if k ⊆ i then f (ordsucc i) else f i) ∈ n.
rewrite the current goal using If_i_1 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).
We will prove f (ordsucc i) ∈ n.
We prove the intermediate claim L1: ordsucc i ∈ ordsucc (ordsucc n).
Apply nat_ordsucc_in_ordsucc to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hi.
Apply ordsuccE n (f (ordsucc i)) (H1 (ordsucc i) L1) to the current goal.
Assume H5: f (ordsucc i) ∈ n.
An exact proof term for the current goal is H5.
Assume H5: f (ordsucc i) = n.
We will prove False.
Apply In_irref i to the current goal.
We will prove i ∈ i.
We prove the intermediate claim L2: k = ordsucc i.
Apply H2 to the current goal.
An exact proof term for the current goal is Hk1.
An exact proof term for the current goal is L1.
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is Hk2.
We prove the intermediate claim L3: i ∈ k.
rewrite the current goal using L2 (from left to right).
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H4 i L3.
Assume H4: ¬ (k ⊆ i).
We will prove (if k ⊆ i then f (ordsucc i) else f i) ∈ n.
rewrite the current goal using If_i_0 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).
We will prove f i ∈ n.
Apply ordsuccE n (f i) (H1 i (ordsuccI1 (ordsucc n) i Hi)) to the current goal.
Assume H5: f i ∈ n.
An exact proof term for the current goal is H5.
Assume H5: f i = n.
We will prove False.
Apply H4 to the current goal.
We will prove k ⊆ i.
We prove the intermediate claim L2: k = i.
Apply H2 to the current goal.
An exact proof term for the current goal is Hk1.
An exact proof term for the current goal is ordsuccI1 (ordsucc n) i Hi.
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is Hk2.
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is (λx Hx ⇒ Hx).
We will prove ∀i j ∈ ordsucc n, f' i = f' j → i = j.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
We will prove (if k ⊆ i then f (ordsucc i) else f i) = (if k ⊆ j then f (ordsucc j) else f j) → i = j.
We prove the intermediate claim Li1: i ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate claim Li2: ordsucc i ∈ ordsucc (ordsucc n).
Apply nat_ordsucc_in_ordsucc to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hi.
We prove the intermediate claim Lj1: j ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
We prove the intermediate claim Lj2: ordsucc j ∈ ordsucc (ordsucc n).
Apply nat_ordsucc_in_ordsucc to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hj.
Apply xm (k ⊆ i) to the current goal.
Assume H4: k ⊆ i.
rewrite the current goal using If_i_1 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).
Apply xm (k ⊆ j) to the current goal.
Assume H5: k ⊆ j.
rewrite the current goal using If_i_1 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f (ordsucc i) = f (ordsucc j) → i = j.
Assume H6.
Apply ordsucc_inj to the current goal.
We will prove ordsucc i = ordsucc j.
An exact proof term for the current goal is H2 (ordsucc i) Li2 (ordsucc j) Lj2 H6.
Assume H5: ¬ (k ⊆ j).
rewrite the current goal using If_i_0 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f (ordsucc i) = f j → i = j.
Assume H6.
We will prove False.
We prove the intermediate claim L3: ordsucc i = j.
Apply H2 to the current goal.
An exact proof term for the current goal is Li2.
An exact proof term for the current goal is Lj1.
An exact proof term for the current goal is H6.
Apply H5 to the current goal.
rewrite the current goal using L3 (from right to left).
Let x be given.
Assume Hx: x ∈ k.
Apply ordsuccI1 to the current goal.
Apply H4 to the current goal.
An exact proof term for the current goal is Hx.
Assume H4: ¬ (k ⊆ i).
rewrite the current goal using If_i_0 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).
Apply xm (k ⊆ j) to the current goal.
Assume H5: k ⊆ j.
rewrite the current goal using If_i_1 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f i = f (ordsucc j) → i = j.
Assume H6.
We will prove False.
We prove the intermediate claim L3: i = ordsucc j.
Apply H2 to the current goal.
An exact proof term for the current goal is Li1.
An exact proof term for the current goal is Lj2.
An exact proof term for the current goal is H6.
Apply H4 to the current goal.
rewrite the current goal using L3 (from left to right).
Let x be given.
Assume Hx: x ∈ k.
Apply ordsuccI1 to the current goal.
Apply H5 to the current goal.
An exact proof term for the current goal is Hx.
Assume H5: ¬ (k ⊆ j).
rewrite the current goal using If_i_0 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f i = f j → i = j.
Apply H2 to the current goal.
An exact proof term for the current goal is Li1.
An exact proof term for the current goal is Lj1.
Assume H3: ¬ (∃i ∈ ordsucc (ordsucc n), f i = n).
Apply IH f to the current goal.
We will prove ∀i ∈ ordsucc n, f i ∈ n.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Apply ordsuccE n (f i) (H1 i (ordsuccI1 (ordsucc n) i Hi)) to the current goal.
Assume Hfi: f i ∈ n.
An exact proof term for the current goal is Hfi.
Assume Hfi: f i = n.
Apply H3 to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is Hfi.
We will prove ∀i j ∈ ordsucc n, f i = f j → i = j.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Apply H2 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
∎