`{Funext} {A : Type} (P : forall n, FinSeq n A -> Type) (z : P 0 fsnil) (s : forall n a (v : FinSeq n A), P n v -> P n.+1 (fscons a v)) {n : nat} (v : FinSeq n A) : P n v. Proof. induction n. - exact (transport (P 0) (path_fsnil v) z). - refine (transport (P n.+1) (path_expand_fscons v) _). apply s. apply IHn. Defined.
Require Import