proposition: Lemma list_map {A B} (f: A → B) (l: ne_list A) : to_list (map f l) = list.map f (to_list l).
proof: Proof. induction l. - reflexivity. - cbn. rewrite <- IHl. reflexivity. Qed.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat