{T} (y x: ne_list T): InList x (to_list (tails y)) → leq (length (to_list x)) (length (to_list y)). Proof. induction y; cbn. - intros [[] | C]. + constructor. + elim C. - intros [[] | C]. + exact _. + by apply leq_succ_r, IHy. Qed.
Require Import