Let Y, u, r and v be given.
Assume Hur: order_rel Y u r.
Assume Hrv: order_rel Y r v.
We will prove between_in_order Y u r v.
We will prove (order_rel Y u r ∧ order_rel Y r v) ∨ (order_rel Y v r ∧ order_rel Y r u) ∨ r = u ∨ r = v.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is (andI (order_rel Y u r) (order_rel Y r v) Hur Hrv).
∎