{A} (n : nat) (a : A) (v : FinSeq (nat_pred n) A) (i : Fin n) : path_fscons' n (idpath a) (fun j => idpath (v j)) i = idpath. Proof. induction i using fin_ind; unfold path_fscons'. - rewrite fin_ind_beta_zero. refine (ap (fun p => p @ _) (concat_p1 _) @ _). apply concat_pV. - rewrite fin_ind_beta_fsucc. refine (ap (fun p => p @ _) (concat_p1 _) @ _). apply concat_pV. Qed.
Require Import