proposition: Lemma path_expand_fscons_fscons' {A : Type} (n : nat) (N : n > 0) (a : A) (v : FinSeq (pred n) A) (i : Fin n) : path_expand_fscons' n i N (fscons' n a v) = path_fscons' n (compute_fshead' n N a v) (compute_fstail' n a v) i.
proof: Proof. induction i using fin_ind; unfold path_fscons', path_expand_fscons'. - do 2 rewrite compute_fin_ind_fin_zero. refine (_ @ concat_p_pp _ _ _). refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^). exact (concat_p1 _)^. - do 2 rewrite compute_fin_ind_fsucc. refine (_ @ concat_p_pp _ _ _). refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^). exact (concat_p1 _)^. Qed.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core