proposition: Lemma compute_finseq_ind_fscons `{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: Proof. simpl. induction (path_expand_fscons_fscons a v)^. set (p1 := compute_fshead a v). set (p2 := compute_fstail a v). induction p1, p2. exact (ap (fun p => transport _ p _) (compute_path_fscons _ _)). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core