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