proposition: Lemma path_expand_fscons_fscons `{Funext} {A : Type} {n : nat} (a : A) (v : FinSeq n A) : path_expand_fscons (fscons a v) = path_fscons (compute_fshead a v) (compute_fstail a v).
proof: Proof. refine (ap (path_forall _ _) _). funext i. pose (p := eisretr apD10 (compute_fstail' n.+1 a v)). refine (_ @ (ap (fun f => _ f i) p)^). exact (path_expand_fscons_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