locator' x -> locator x. Proof. intros l' q r nu. destruct (dec (locates_right l' nu)) as [yes|no]. - apply inl. exact (locates_right_true l' nu yes). - apply inr. exact (locates_right_false l' nu no). Defined.
Require Import