fact: Fixpoint from_list (x: T) (xs: list T): ne_list := match xs with | nil => one x | Datatypes.cons h t => cons x (from_list h t) end.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat