proposition: Lemma desc_tail : forall (x:List) (a b:A), Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
proof: Proof. intro. apply rev_ind with (A := A) (P := fun x:List => forall a b:A, Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b). intros. inversion H. cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil); auto with sets; intro. generalize H0. intro. generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4); simple induction 1. intros. generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. generalize H1. rewrite <- H10; rewrite <- H7; intro. apply (t_step A leA); auto with sets. intros. inversion H0. generalize (app_cons_not_nil _ _ _ H3); intro. elim H1. generalize H0. generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b); simple induction 1. intro. generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro. generalize (H x0 b H6). intro. apply t_trans with (A := A) (y := x0); auto with sets. apply t_step. generalize H1. rewrite H4; intro. generalize (app_inj_tail _ _ _ _ H8); simple induction 1. intros. generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b). intro. generalize H10. rewrite H12; intro. generalize (app_inj_tail _ _ _ _ H13); simple induction 1. intros. rewrite <- H11; rewrite <- H16; auto with sets. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)