`{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)) : finseq_ind P z s fsnil = z. Proof. exact (ap (fun x => _ x z) (hset_path2 1 (path_fsnil fsnil)))^. Defined.
Require Import