fact: Definition fscons' {A : Type} (n : nat) (a : A) (v : FinSeq (pred n) A) : FinSeq n A := fun i => fin_rec (fun n => FinSeq (pred n) A -> A) (fun _ _ => a) (fun n' i _ v => v i) i v.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core