Let k be given.
Assume HkOmega.
We prove the intermediate claim HsuccOmega: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkOmega).
We will prove order_rel (setprod 2 ω) (0,k) (0,ordsucc k).
We will prove (setprod 2 ω = R ∧ Rlt (0,k) (0,ordsucc k)) ∨ (setprod 2 ω = rational_numbers ∧ Rlt (0,k) (0,ordsucc k)) ∨ (setprod 2 ω = ω ∧ (0,k) ∈ (0,ordsucc k)) ∨ (setprod 2 ω = ω ∖ {0} ∧ (0,k) ∈ (0,ordsucc k)) ∨ (setprod 2 ω = setprod 2 ω ∧ ∃i m j n0 : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n0 ∈ ω ∧ (0,k) = (i,m) ∧ (0,ordsucc k) = (j,n0) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n0))) ∨ (setprod 2 ω = setprod R R ∧ ∃a1 a2 b1 b2 : set, (0,k) = (a1,a2) ∧ (0,ordsucc k) = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal (setprod 2 ω) ∧ setprod 2 ω ≠ R ∧ setprod 2 ω ≠ rational_numbers ∧ setprod 2 ω ≠ setprod 2 ω ∧ setprod 2 ω ≠ setprod R R ∧ (0,k) ∈ (0,ordsucc k)).
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod 2 ω = setprod 2 ω ∧ ∃i m j n0 : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n0 ∈ ω ∧ (0,k) = (i,m) ∧ (0,ordsucc k) = (j,n0) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n0)).
Apply andI to the current goal.
Use reflexivity.
We use 0 to witness the existential quantifier.
We use k to witness the existential quantifier.
We use 0 to witness the existential quantifier.
We use (ordsucc k) to witness the existential quantifier.
We prove the intermediate claim Heq0k: (0,k) = (0,k).
Use reflexivity.
We prove the intermediate claim Heq0sk: (0,ordsucc k) = (0,ordsucc k).
Use reflexivity.
We prove the intermediate claim H12: 0 ∈ 2 ∧ k ∈ ω.
An exact proof term for the current goal is (andI (0 ∈ 2) (k ∈ ω) In_0_2 HkOmega).
We prove the intermediate claim H123: (0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2.
An exact proof term for the current goal is (andI (0 ∈ 2 ∧ k ∈ ω) (0 ∈ 2) H12 In_0_2).
We prove the intermediate claim H1234: ((0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2) ∧ ordsucc k ∈ ω.
An exact proof term for the current goal is (andI ((0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2) (ordsucc k ∈ ω) H123 HsuccOmega).
We prove the intermediate claim H12345: (((0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2) ∧ ordsucc k ∈ ω) ∧ (0,k) = (0,k).
An exact proof term for the current goal is (andI (((0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2) ∧ ordsucc k ∈ ω) ((0,k) = (0,k)) H1234 Heq0k).
We prove the intermediate claim H123456: ((((0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2) ∧ ordsucc k ∈ ω) ∧ (0,k) = (0,k)) ∧ (0,ordsucc k) = (0,ordsucc k).
An exact proof term for the current goal is (andI ((((0 ∈ 2 ∧ k ∈ ω) ∧ 0 ∈ 2) ∧ ordsucc k ∈ ω) ∧ (0,k) = (0,k)) ((0,ordsucc k) = (0,ordsucc k)) H12345 Heq0sk).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
We prove the intermediate claim HkInSucc: k ∈ ordsucc k.
An exact proof term for the current goal is (ordsuccI2 k).
We prove the intermediate claim Hlex: 0 ∈ 0 ∨ (0 = 0 ∧ k ∈ ordsucc k).
An exact proof term for the current goal is (orIR (0 ∈ 0) (0 = 0 ∧ k ∈ ordsucc k) (andI (0 = 0) (k ∈ ordsucc k) H00 HkInSucc)).
Apply andI to the current goal.
An exact proof term for the current goal is H123456.
An exact proof term for the current goal is Hlex.
∎