path_expand_fscons_fscons' {A : Type} (n : nat) (N : n > 0) (a : A) (v : FinSeq (nat_pred n) A) (i : Fin n) : path_expand_fscons' n i N (fscons' n a v) = path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i. Proof. induction i using fin_ind; unfold path_fscons', path_expand_fscons'. - do 2 rewrite fin_ind_beta_zero. refine (_ @ concat_p_pp _ _ _). refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^). exact (concat_p1 _)^. - do 2 rewrite fin_ind_beta_fsucc. refine (_ @ concat_p_pp _ _ _). refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^). exact (concat_p1 _)^. Qed.
Require Import