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