`{Funext} {A} {n} (a : A) (v : FinSeq n A) : path_fscons (idpath a) (idpath v) = idpath. Proof. refine (ap (path_forall _ _) _ @ eta_path_forall _ _ _). funext i. exact (path_fscons'_beta n.+1 a v i). Defined.
Require Import