Let Y, u and v be given.

We will prove between_in_order Y u v v.

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

Apply orIR to the current goal.

Use reflexivity.

∎