proposition: Lemma path_expand_fscons' {A : Type} (n : nat) (i : Fin n) (N : n > 0) (v : FinSeq n A) : fscons' n (fshead' n N v) (fstail' n v) i = v i.
proof: Proof. induction i using fin_ind. - apply compute_fshead. - apply (compute_fstail' n.+1 (fshead v) (fstail v)). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core