{A : Type} (l : list A) (i : nat) (p : nat_pred (length l) = i) : nth l i = last l. Proof. destruct p. induction l as [|a l IHl]. 1: reflexivity. destruct l as [|b l]. 1: reflexivity. cbn; apply IHl. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum