proposition: Lemma desc_end : forall (a b : A) (x : List), Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] -> 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 [a] a0). intros E; rewrite <- E; intros. generalize (desc_tail l a a0 H0); intro. inversion H1. + eapply clos_rt_t; [ eassumption | apply t_step; assumption ]. + inversion H4. Qed.
imports: List Relation_Operators Operators_Properties Transitive_Closure