Let a and b be given.
Assume Hab.
We will prove order_rel R a b.
We will prove (R = R ∧ Rlt a b) ∨ (R = rational_numbers ∧ Rlt a b) ∨ (R = ω ∧ a ∈ b) ∨ (R = ω ∖ {0} ∧ a ∈ b) ∨ (R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (R = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal R ∧ R ≠ R ∧ R ≠ rational_numbers ∧ R ≠ setprod 2 ω ∧ R ≠ setprod R R ∧ a ∈ b).
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
We will prove R = R ∧ Rlt a b.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hab.
∎