proposition: Lemma compute_path_fscons `{Funext} {A} {n} (a : A) (v : FinSeq n A) : path_fscons (idpath a) (idpath v) = idpath.
proof: Proof. refine (ap (path_forall _ _) _ @ eta_path_forall _ _ _). funext i. exact (compute_path_fscons' n.+1 a v i). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core