proposition: Lemma ltl_unit : forall (x : List) (a b : A), Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b].
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: List Relation_Operators Operators_Properties Transitive_Closure