`{Funext} {A : Type} (P : forall n, FinSeq n A -> Type) (z : P 0 fsnil) (s : forall (n : nat) (a : A) (v : FinSeq n A), P n v -> P n.+1 (fscons a v)) {n : nat} (a : A) (v : FinSeq n A) : finseq_ind P z s (fscons a v) = s n a v (finseq_ind P z s v). Proof. simpl. induction (path_expand_fscons_fscons a v)^. set (p1 := fshead_beta_fscons a v). set (p2 := fstail_beta_fscons a v). induction p1, p2. exact (ap (fun p => transport _ p _) (path_fscons_beta _ _)). Defined.
Require Import