locator (meet x y). Proof. intros q r ltqr. destruct (l q r ltqr, m q r ltqr) as [[ltqx|ltxr] [ltqy|ltyr]]. - apply inl, meet_lt_l; assumption. - apply inr, meet_lt_r_r; assumption. - apply inr, meet_lt_r_l; assumption. - apply inr, meet_lt_r_r; assumption. Qed.
Require Import