Let Y, u and v be given.

We will prove between_in_order Y u u v.

We will prove (order_rel Y u u ∧ order_rel Y u v) ∨ (order_rel Y v u ∧ order_rel Y u u) ∨ u = u ∨ u = v.

Apply orIL to the current goal.

Apply orIR to the current goal.

Use reflexivity.

∎