proposition: Lemma decomp_eq (l: ne_list): l = from_list (head l) (tail l).
proof: Proof. Proof with auto. induction l... destruct l... cbn in *. rewrite IHl... Qed.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat