proposition: Lemma path_expand_fscons `{Funext} {A} {n} (v : FinSeq n.+1 A) : fscons (fshead v) (fstail v) = v.
proof: Proof. funext i. apply path_expand_fscons'. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core