Let n be given.
Assume Hn.
Let f be given.
Assume Hf1 Hf2.
We will prove (∀i ∈ n, f i ∈ n) ∧ (∀i j ∈ n, f i = f j → i = j) ∧ (∀j ∈ n, ∃i ∈ n, f i = j).
Apply and3I to the current goal.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is Hf2.
Let j be given.
Assume Hj: j ∈ n.
Apply dneg to the current goal.
Assume H1: ¬ ∃i ∈ n, f i = j.
Set f' to be the term λi : set ⇒ if i = n then j else f i.
Apply PigeonHole_nat n Hn f' to the current goal.
We will prove ∀i ∈ ordsucc n, f' i ∈ n.
Let i be given.
Assume Hi.
We will prove (if i = n then j else f i) ∈ n.
Apply xm (i = n) to the current goal.
Assume H1: i = n.
rewrite the current goal using If_i_1 (i = n) j (f i) H1 (from left to right).
We will prove j ∈ n.
An exact proof term for the current goal is Hj.
Assume H1: i ≠ n.
rewrite the current goal using If_i_0 (i = n) j (f i) H1 (from left to right).
We will prove f i ∈ n.
Apply Hf1 to the current goal.
Apply ordsuccE n i Hi to the current goal.
Assume H2: i ∈ n.
An exact proof term for the current goal is H2.
Assume H2: i = n.
Apply H1 H2 to the current goal.
We will prove ∀i k ∈ ordsucc n, f' i = f' k → i = k.
Let i be given.
Assume Hi.
Let k be given.
Assume Hk.
We prove the intermediate claim Li: i ≠ n → i ∈ n.
Assume Hin: i ≠ n.
Apply ordsuccE n i Hi to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2.
Apply Hin H2 to the current goal.
We prove the intermediate claim Lk: k ≠ n → k ∈ n.
Assume Hkn: k ≠ n.
Apply ordsuccE n k Hk to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2.
Apply Hkn H2 to the current goal.
We will prove (if i = n then j else f i) = (if k = n then j else f k) → i = k.
Apply xm (i = n) to the current goal.
Assume H2: i = n.
Apply xm (k = n) to the current goal.
Assume H3: k = n.
Assume _.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is H2.
Assume H3: k ≠ n.
rewrite the current goal using If_i_1 (i = n) j (f i) H2 (from left to right).
rewrite the current goal using If_i_0 (k = n) j (f k) H3 (from left to right).
Assume H4: j = f k.
Apply H1 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
We will prove k ∈ n.
An exact proof term for the current goal is Lk H3.
Use symmetry.
An exact proof term for the current goal is H4.
Assume H2: i ≠ n.
Apply xm (k = n) to the current goal.
Assume H3: k = n.
rewrite the current goal using If_i_0 (i = n) j (f i) H2 (from left to right).
rewrite the current goal using If_i_1 (k = n) j (f k) H3 (from left to right).
Assume H4: f i = j.
Apply H1 to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
We will prove i ∈ n.
An exact proof term for the current goal is Li H2.
An exact proof term for the current goal is H4.
Assume H3: k ≠ n.
rewrite the current goal using If_i_0 (i = n) j (f i) H2 (from left to right).
rewrite the current goal using If_i_0 (k = n) j (f k) H3 (from left to right).
We will prove f i = f k → i = k.
Apply Hf2 to the current goal.
We will prove i ∈ n.
An exact proof term for the current goal is Li H2.
We will prove k ∈ n.
An exact proof term for the current goal is Lk H3.
∎