proposition: Lemma desc_tail : forall (x : List) (a b : A), Descl (b :: x ++ [a]) -> clos_refl_trans A leA a b.
proof: Proof. intro. apply rev_ind with (P := fun x : List => forall a b : A, Descl (b :: x ++ [a]) -> clos_refl_trans A leA a b); intros. - inversion H. assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets. destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-). inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ]. - inversion H0. + apply app_cons_not_nil in H3 as []. + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0. pose proof (H x0 b H0). apply rt_trans with (y := x0); auto with sets. enough (H5 : clos_refl A leA a x0) by (inversion H5; subst; [ apply rt_step | apply rt_refl ]; assumption). apply app_inj_tail in H1 as (H1, ->). rewrite app_comm_cons in H1. apply app_inj_tail in H1 as (_, <-). assumption. Qed.
imports: List Relation_Operators Operators_Properties Transitive_Closure