proposition: Lemma desc_end : forall (a b:A) (x:List), Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) -> clos_trans A leA a b.
proof: Proof. intros a b x. case x. simpl. simple induction 1. intros. inversion H1; auto with sets. inversion H3. simple induction 1. generalize (app_comm_cons l (Cons a Nil) a0). intros E; rewrite <- E; intros. generalize (desc_tail l a a0 H0); intro. inversion H1. apply t_trans with (y := a0); auto with sets. inversion H4. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)