proposition: Lemma tl_length (l: ne_list) : S (length (tl (to_list l))) = length (to_list l).
proof: Proof. destruct l; reflexivity. Qed.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat