{A : Type} (l : list A) (n : nat) (x : A) (H : (n < length l)%nat) (H' : (n.+1 < length (x :: l))%nat) : nth' (x :: l) n.+1 H' = nth' l n H. Proof. apply isinj_some. nrefine (_^ @ _ @ _). 1,3: rapply nth_nth'. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum