`{Funext} {A : Type} {n : nat} (a : A) (v : FinSeq n A) : path_expand_fscons (fscons a v) = path_fscons (fshead_beta_fscons a v) (fstail_beta_fscons a v). Proof. refine (ap (path_forall _ _) _). funext i. pose (p := eisretr apD10 (fstail'_beta_fscons' n.+1 a v)). refine (_ @ (ap (fun f => _ f i) p)^). exact (' n.+1 _ a v i). Defined.
Require Import