(x : F) : locator x. Proof. intros q r ltqr. case (LEM (' q < x)). - apply _. - exact inl. - intros notlt. apply inr. assert (ltqr' : ' q < ' r) by auto. exact (nlt_lt_trans notlt ltqr'). Qed.
Require Import