proposition: Lemma nth_member_nth_error : forall ls p, nth_member ls (to_nat (projT2 p)) = Some p <-> nth_error ls (to_nat (projT2 p)) = Some (projT1 p).
proof: Proof. destruct p. simpl in *. induction m. { simpl. split; auto. } { simpl. split. { intros. destruct (nth_member ls (to_nat m)); try congruence. { destruct s. inv_all. subst. inv_all. subst. apply IHm. reflexivity. } } { intros. eapply IHm in H. rewrite H. reflexivity. } } Qed.
imports: Coq.Lists.List Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics.Injection ExtLib.Tactics.EqDep