fact: Fixpoint take (n: nat) (l: ne_list): ne_list := match l, n with | cons x xs, S n' => take n' xs | _, _ => one (head l) end.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat