Let Y, u, r and v be given.
Assume Hvr: order_rel Y v r.
Assume Hru: order_rel Y r u.
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 orIR to the current goal.
An exact proof term for the current goal is (andI (order_rel Y v r) (order_rel Y r u) Hvr Hru).
∎