proposition: Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
proof: Proof. unfold well_founded at 2. simple induction a; intros x y. apply Acc_intro. simple induction y0. unfold lex_exp at 1; simpl. apply rev_ind with (A := A) (P := fun x:List => forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>). intros. inversion_clear H0. intro. generalize (well_founded_ind (wf_clos_trans A leA H)). intros GR. apply GR with (P := fun x0:A => forall l:List, (forall (x1:List) (y:Descl x1), ltl x1 l -> Acc Lex_Exp << x1, y >>) -> forall (x1:List) (y:Descl x1), ltl x1 (l ++ Cons x0 Nil) -> Acc Lex_Exp << x1, y >>). intro; intros HInd; intros. generalize (right_prefix x2 l (Cons x1 Nil) H1). simple induction 1. intro; apply (H0 x2 y1 H3). simple induction 1. intro; simple induction 1. clear H4 H2. intro; generalize y1; clear y1. rewrite H2. apply rev_ind with (A := A) (P := fun x3:List => forall y1:Descl (l ++ x3), ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>). intros. generalize (sym_eq (app_nil_r l)); intros Heq. generalize y1. clear y1. rewrite <- Heq. intro. apply Acc_intro. simple induction y2. unfold lex_exp at 1. simpl; intros x4 y3. intros. apply (H0 x4 y3); auto with sets. intros. generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1). simple induction 1. intros. generalize (desc_end x4 x1 l0 (conj H8 H5)); intros. generalize y1. rewrite (app_assoc l l0 (Cons x4 Nil)); intro. generalize (HInd x4 H9 (l ++ l0)); intros HInd2. generalize (ltl_unit l0 x4 x1 H8 H5); intro. generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2). simple induction 1; intros. generalize (H4 H12 H10); intro. generalize (Acc_inv H14). generalize (acc_app l l0 H12 H14). intros f g. generalize (HInd2 f); intro. apply Acc_intro. simple induction y3. unfold lex_exp at 1; simpl; intros. apply H15; auto with sets. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)