proposition: Lemma compute_finseq_ind_fsnil `{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: Proof. exact (ap (fun x => _ x z) (hset_path2 1 (path_fsnil fsnil)))^. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core