(l : locator x) : locator'_locator (locator_locator' l) = l. Proof. apply path_forall; intros q. apply path_forall; intros r. apply path_forall; intros nu. unfold locator'_locator, locator_locator'. simpl. destruct (l q r nu); auto. Qed.
Require Import