fact: Definition fstail' {A} (n : nat) : FinSeq n A -> FinSeq (pred n) A := match n with | 0 => fun _ => Empty_rec | n'.+1 => fun v i => v (fsucc i) end.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction HoTT.Spaces.Nat.Core