path_list_nth'@{i|} {A : Type@{i}} (l l' : list A) (p : length l = length l') : (forall n (H : (n < length l)%nat), nth' l n H = nth' l' n (p # H)) -> l = l'. Proof. intros H. induction l as [|a l IHl] in l', p, H |- * using list_ind@{i i}. { destruct l'. - reflexivity. - discriminate. } destruct l' as [|a' l']. 1: discriminate. f_ap. - exact (H 0%nat _). - snrapply IHl. 1: by apply path_nat_succ. intros n Hn. snrefine ((nth'_cons l n a Hn _)^ @ _). 1: apply leq_succ, Hn. lhs nrapply H. nrapply nth'_cons. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum