locator_locator' : locator x -> locator' x. Proof. intros l. refine (Build_locator' x (fun q r nu => Build_DHProp (Build_HProp (is_inl (l q r nu))) _) _ _). - intros q r nu. simpl. apply un_inl. - intros q r nu. simpl. destruct (l q r nu) as [ltqx|]. + simpl; intros f; destruct (f tt). + intros ?; assumption. Defined.
Require Import