proposition: Lemma tails_are_shorter {T} (y x: ne_list T): InList x (to_list (tails y)) → leq (length (to_list x)) (length (to_list y)).
proof: Proof. Proof with auto. induction y; cbn. - intros [[] | C]. + constructor. + elim C. - intros [[] | C]... Qed.
imports: HoTT.Utf8Minimal HoTT.Classes.implementations.list HoTT.Basics.Overture HoTT.Spaces.Nat