Let k and n be given.
Assume HkOmega.
Assume HnOmega.
We will prove order_rel (setprod 2 ω) (0,k) (1,n).
We will prove (setprod 2 ω = R ∧ Rlt (0,k) (1,n)) ∨ (setprod 2 ω = rational_numbers ∧ Rlt (0,k) (1,n)) ∨ (setprod 2 ω = ω ∧ (0,k) ∈ (1,n)) ∨ (setprod 2 ω = ω ∖ {0} ∧ (0,k) ∈ (1,n)) ∨ (setprod 2 ω = setprod 2 ω ∧ ∃i m j n0 : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n0 ∈ ω ∧ (0,k) = (i,m) ∧ (1,n) = (j,n0) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n0))) ∨ (setprod 2 ω = setprod R R ∧ ∃a1 a2 b1 b2 : set, (0,k) = (a1,a2) ∧ (1,n) = (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) ∈ (1,n)).
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) ∧ (1,n) = (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 1 to witness the existential quantifier.
We use n to witness the existential quantifier.
We prove the intermediate claim Heq0k: (0,k) = (0,k).
Use reflexivity.
We prove the intermediate claim Heq1n: (1,n) = (1,n).
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 ∈ ω) ∧ 1 ∈ 2.
An exact proof term for the current goal is (andI (0 ∈ 2 ∧ k ∈ ω) (1 ∈ 2) H12 In_1_2).
We prove the intermediate claim H1234: ((0 ∈ 2 ∧ k ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω.
An exact proof term for the current goal is (andI ((0 ∈ 2 ∧ k ∈ ω) ∧ 1 ∈ 2) (n ∈ ω) H123 HnOmega).
We prove the intermediate claim H12345: (((0 ∈ 2 ∧ k ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ∧ (0,k) = (0,k).
An exact proof term for the current goal is (andI (((0 ∈ 2 ∧ k ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ((0,k) = (0,k)) H1234 Heq0k).
We prove the intermediate claim H123456: ((((0 ∈ 2 ∧ k ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ∧ (0,k) = (0,k)) ∧ (1,n) = (1,n).
An exact proof term for the current goal is (andI ((((0 ∈ 2 ∧ k ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ∧ (0,k) = (0,k)) ((1,n) = (1,n)) H12345 Heq1n).
We prove the intermediate claim Hlex: 0 ∈ 1 ∨ (0 = 1 ∧ k ∈ n).
An exact proof term for the current goal is (orIL (0 ∈ 1) (0 = 1 ∧ k ∈ n) In_0_1).
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.
∎