fact: Fixpoint map {A B} (f: A → B) (l: ne_list A): ne_list B := match l with | one x => one (f x) | cons h t => cons (f h) (map f t) end.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat