proposition: Lemma ltl_unit : forall (x:List) (a b:A), Descl (x ++ Cons a Nil) -> ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil).
proof: Proof. intro. case x. intros; apply (Lt_nil A leA). simpl; intros. inversion_clear H0. apply (Lt_hd A leA a b); auto with sets. inversion_clear H1. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)