Lexicographic_Exponentiation.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Author: Cristina Cornes

From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355

Require Import List.
Require Import Relation_Operators.
Require Import Operators_Properties.
Require Import Transitive_Closure.

Import ListNotations.

Section Wf_Lexicographic_Exponentiation.
  Variable A : Set.
  Variable leA : A -> A -> Prop.

  Notation Power := (Pow A leA).
  Notation Lex_Exp := (lex_exp A leA).
  Notation ltl := (Ltl A leA).
  Notation Descl := (Desc A leA).

  Notation List := (list A).
  Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).

  (* Hint Resolve d_one d_nil t_step. *)

  Lemma left_prefix : forall x y z : List, ltl (x ++ y) z -> ltl x z.A:Set
leA:A -> A -> Prop
forall x y z : List, ltl (x ++ y) z -> ltl x z
  Proof.A:Set
leA:A -> A -> Prop
forall x y z : List, ltl (x ++ y) z -> ltl x z
    simple induction x.A:Set
leA:A -> A -> Prop
x:List
forall y z : List, ltl ([] ++ y) z -> ltl [] z
A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List),
(forall y z : List, ltl (l ++ y) z -> ltl l z) ->
forall y z : List,
ltl ((a :: l) ++ y) z -> ltl (a :: l) z
    simple induction z.A:Set
leA:A -> A -> Prop
x, y, z:List
ltl ([] ++ y) [] -> ltl [] []
A:Set
leA:A -> A -> Prop
x, y, z:List
forall (a : A) (l : List),
(ltl ([] ++ y) l -> ltl [] l) ->
ltl ([] ++ y) (a :: l) -> ltl [] (a :: l)
A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List),
(forall y z : List, ltl (l ++ y) z -> ltl l z) ->
forall y z : List,
ltl ((a :: l) ++ y) z -> ltl (a :: l) z
    simpl; intros H.A:Set
leA:A -> A -> Prop
x, y, z:List
H:ltl y []
ltl [] []
A:Set
leA:A -> A -> Prop
x, y, z:List
forall (a : A) (l : List),
(ltl ([] ++ y) l -> ltl [] l) ->
ltl ([] ++ y) (a :: l) -> ltl [] (a :: l)
A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List),
(forall y z : List, ltl (l ++ y) z -> ltl l z) ->
forall y z : List,
ltl ((a :: l) ++ y) z -> ltl (a :: l) z
    inversion_clear H.A:Set
leA:A -> A -> Prop
x, y, z:List
forall (a : A) (l : List),
(ltl ([] ++ y) l -> ltl [] l) ->
ltl ([] ++ y) (a :: l) -> ltl [] (a :: l)
A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List),
(forall y z : List, ltl (l ++ y) z -> ltl l z) ->
forall y z : List,
ltl ((a :: l) ++ y) z -> ltl (a :: l) z
    simpl; intros; apply (Lt_nil A leA).A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List),
(forall y z : List, ltl (l ++ y) z -> ltl l z) ->
forall y z : List,
ltl ((a :: l) ++ y) z -> ltl (a :: l) z
    intros a l HInd.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y z : List, ltl (l ++ y) z -> ltl l z
forall y z : List,
ltl ((a :: l) ++ y) z -> ltl (a :: l) z
    simpl.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y z : List, ltl (l ++ y) z -> ltl l z
forall y z : List,
ltl (a :: l ++ y) z -> ltl (a :: l) z
    intros.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y0 z0 : List,
ltl (l ++ y0) z0 -> ltl l z0
y, z:List
H:ltl (a :: l ++ y) z
ltl (a :: l) z
    inversion_clear H.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y1 z0 : List,
ltl (l ++ y1) z0 -> ltl l z0
y, z:List
b:A
y0:List
H0:leA a b
ltl (a :: l) (b :: y0)
A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y1 z0 : List,
ltl (l ++ y1) z0 -> ltl l z0
y, z, y0:List
H0:ltl (l ++ y) y0
ltl (a :: l) (a :: y0)
    apply (Lt_hd A leA); auto with sets.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y1 z0 : List,
ltl (l ++ y1) z0 -> ltl l z0
y, z, y0:List
H0:ltl (l ++ y) y0
ltl (a :: l) (a :: y0)
    apply (Lt_tl A leA).A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
HInd:forall y1 z0 : List,
ltl (l ++ y1) z0 -> ltl l z0
y, z, y0:List
H0:ltl (l ++ y) y0
ltl l y0
    apply (HInd y y0); auto with sets.
  Qed.


  Lemma right_prefix :
    forall x y z : List,
      ltl x (y ++ z) ->
      ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).A:Set
leA:A -> A -> Prop
forall x y z : List,
ltl x (y ++ z) ->
ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z)
  Proof.A:Set
leA:A -> A -> Prop
forall x y z : List,
ltl x (y ++ z) ->
ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z)
    intros x y; generalize x.A:Set
leA:A -> A -> Prop
x, y:List
forall x0 z : List,
ltl x0 (y ++ z) ->
ltl x0 y \/
(exists y' : List, x0 = y ++ y' /\ ltl y' z)
    elim y; simpl.A:Set
leA:A -> A -> Prop
x, y:List
forall x0 z : List,
ltl x0 z ->
ltl x0 [] \/ (exists y' : List, x0 = y' /\ ltl y' z)
A:Set
leA:A -> A -> Prop
x, y:List
forall (a : A) (l : List),
(forall x0 z : List,
 ltl x0 (l ++ z) ->
 ltl x0 l \/
 (exists y' : List, x0 = l ++ y' /\ ltl y' z)) ->
forall x0 z : List,
ltl x0 (a :: l ++ z) ->
ltl x0 (a :: l) \/
(exists y' : List, x0 = a :: l ++ y' /\ ltl y' z)
    right.A:Set
leA:A -> A -> Prop
x, y, x0, z:List
H:ltl x0 z
exists y' : List, x0 = y' /\ ltl y' z
A:Set
leA:A -> A -> Prop
x, y:List
forall (a : A) (l : List),
(forall x0 z : List,
 ltl x0 (l ++ z) ->
 ltl x0 l \/
 (exists y' : List, x0 = l ++ y' /\ ltl y' z)) ->
forall x0 z : List,
ltl x0 (a :: l ++ z) ->
ltl x0 (a :: l) \/
(exists y' : List, x0 = a :: l ++ y' /\ ltl y' z)
    exists x0; auto with sets.A:Set
leA:A -> A -> Prop
x, y:List
forall (a : A) (l : List),
(forall x0 z : List,
 ltl x0 (l ++ z) ->
 ltl x0 l \/
 (exists y' : List, x0 = l ++ y' /\ ltl y' z)) ->
forall x0 z : List,
ltl x0 (a :: l ++ z) ->
ltl x0 (a :: l) \/
(exists y' : List, x0 = a :: l ++ y' /\ ltl y' z)
    intros.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x1 z0 : List,
ltl x1 (l ++ z0) ->
ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
ltl x0 (a :: l) \/
(exists y' : List, x0 = a :: l ++ y' /\ ltl y' z)
    inversion H0.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1:List
H1:[] = x0
H3:a0 = a
H4:x1 = l ++ z
ltl [] (a :: l) \/
(exists y' : List, [] = a :: l ++ y' /\ ltl y' z)
A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0, b:A
x1, y0:List
H3:leA a0 a
H2:a0 :: x1 = x0
H1:b = a
H4:y0 = l ++ z
ltl (a0 :: x1) (a :: l) \/
(exists y' : List, a0 :: x1 = a :: l ++ y' /\ ltl y' z)
A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    left; apply (Lt_nil A leA).A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0, b:A
x1, y0:List
H3:leA a0 a
H2:a0 :: x1 = x0
H1:b = a
H4:y0 = l ++ z
ltl (a0 :: x1) (a :: l) \/
(exists y' : List, a0 :: x1 = a :: l ++ y' /\ ltl y' z)
A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    left; apply (Lt_hd A leA); auto with sets.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    generalize (H x1 z H3).A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z) ->
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    simple induction 1.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
H5:ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z)
ltl x1 l ->
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
H5:ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z)
(exists y' : List, x1 = l ++ y' /\ ltl y' z) ->
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    left; apply (Lt_tl A leA); auto with sets.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
H5:ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z)
(exists y' : List, x1 = l ++ y' /\ ltl y' z) ->
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    simple induction 1.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x2 z0 : List,
ltl x2 (l ++ z0) ->
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
H5:ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z)
H6:exists y' : List, x1 = l ++ y' /\ ltl y' z
forall x2 : List,
x1 = l ++ x2 /\ ltl x2 z ->
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    simple induction 1; intros.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x3 z0 : List,
ltl x3 (l ++ z0) ->
ltl x3 l \/
(exists y' : List, x3 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
H5:ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z)
H6:exists y' : List, x1 = l ++ y' /\ ltl y' z
x2:List
H7:x1 = l ++ x2 /\ ltl x2 z
H8:x1 = l ++ x2
H9:ltl x2 z
ltl (a :: x1) (a :: l) \/
(exists y' : List, a :: x1 = a :: l ++ y' /\ ltl y' z)
    rewrite H8.A:Set
leA:A -> A -> Prop
x, y:List
a:A
l:List
H:forall x3 z0 : List,
ltl x3 (l ++ z0) ->
ltl x3 l \/
(exists y' : List, x3 = l ++ y' /\ ltl y' z0)
x0, z:List
H0:ltl x0 (a :: l ++ z)
a0:A
x1, y0:List
H3:ltl x1 (l ++ z)
H2:a0 :: x1 = x0
H1:a0 = a
H4:y0 = l ++ z
H5:ltl x1 l \/
(exists y' : List, x1 = l ++ y' /\ ltl y' z)
H6:exists y' : List, x1 = l ++ y' /\ ltl y' z
x2:List
H7:x1 = l ++ x2 /\ ltl x2 z
H8:x1 = l ++ x2
H9:ltl x2 z
ltl (a :: l ++ x2) (a :: l) \/
(exists y' : List,
   a :: l ++ x2 = a :: l ++ y' /\ ltl y' z)
    right; exists x2; auto with sets.
  Qed.

  Lemma desc_prefix : forall (x : List) (a : A), Descl (x ++ [a]) -> Descl x.A:Set
leA:A -> A -> Prop
forall (x : List) (a : A), Descl (x ++ [a]) -> Descl x
  Proof.A:Set
leA:A -> A -> Prop
forall (x : List) (a : A), Descl (x ++ [a]) -> Descl x
    intros.A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
Descl x
    inversion H.A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
H1:[] = x ++ [a]
Descl x
A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
x0:A
H1:[x0] = x ++ [a]
Descl x
A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
x0, y:A
l:List
H1:clos_refl A leA x0 y
H2:Descl (l ++ [y])
H0:(l ++ [y]) ++ [x0] = x ++ [a]
Descl x
    -A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
H1:[] = x ++ [a]
Descl x apply app_cons_not_nil in H1 as [].
    -A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
x0:A
H1:[x0] = x ++ [a]
Descl x assert (x ++ [a] = [x0]) by auto with sets.A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
x0:A
H1:[x0] = x ++ [a]
H0:x ++ [a] = [x0]
Descl x
      apply app_eq_unit in H0 as [(->, _)| (_, [=])].A:Set
leA:A -> A -> Prop
a:A
H:Descl ([] ++ [a])
x0:A
H1:[x0] = [] ++ [a]
Descl []
      auto using d_nil.
    -A:Set
leA:A -> A -> Prop
x:List
a:A
H:Descl (x ++ [a])
x0, y:A
l:List
H1:clos_refl A leA x0 y
H2:Descl (l ++ [y])
H0:(l ++ [y]) ++ [x0] = x ++ [a]
Descl x apply app_inj_tail in H0 as (<-, _).A:Set
leA:A -> A -> Prop
a, y:A
l:List
H:Descl ((l ++ [y]) ++ [a])
x0:A
H1:clos_refl A leA x0 y
H2:Descl (l ++ [y])
Descl (l ++ [y])
      assumption.
  Qed.

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


  Lemma dist_aux :
    forall z : List,
      Descl z -> forall x y : List, z = x ++ y -> Descl x /\ Descl y.A:Set
leA:A -> A -> Prop
forall z : List,
Descl z ->
forall x y : List, z = x ++ y -> Descl x /\ Descl y
  Proof.A:Set
leA:A -> A -> Prop
forall z : List,
Descl z ->
forall x y : List, z = x ++ y -> Descl x /\ Descl y
    intros z D.A:Set
leA:A -> A -> Prop
z:List
D:Descl z
forall x y : List, z = x ++ y -> Descl x /\ Descl y
    induction D as [| | * H D Hind]; intros.A:Set
leA:A -> A -> Prop
x, y:List
H:[] = x ++ y
Descl x /\ Descl y
A:Set
leA:A -> A -> Prop
x:A
x0, y:List
H:[x] = x0 ++ y
Descl x0 /\ Descl y
A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y1 : List,
l ++ [y] = x1 ++ y1 -> Descl x1 /\ Descl y1
x0, y0:List
H0:(l ++ [y]) ++ [x] = x0 ++ y0
Descl x0 /\ Descl y0
    -A:Set
leA:A -> A -> Prop
x, y:List
H:[] = x ++ y
Descl x /\ Descl y assert (H0 : x ++ y = []) by auto with sets.A:Set
leA:A -> A -> Prop
x, y:List
H:[] = x ++ y
H0:x ++ y = []
Descl x /\ Descl y
      apply app_eq_nil in H0 as (->, ->).A:Set
leA:A -> A -> Prop
H:[] = [] ++ []
Descl [] /\ Descl []
      split; apply d_nil.
    -A:Set
leA:A -> A -> Prop
x:A
x0, y:List
H:[x] = x0 ++ y
Descl x0 /\ Descl y assert (E : x0 ++ y = [x]) by auto with sets.A:Set
leA:A -> A -> Prop
x:A
x0, y:List
H:[x] = x0 ++ y
E:x0 ++ y = [x]
Descl x0 /\ Descl y
      apply app_eq_unit in E as [(->, ->)| (->, ->)].A:Set
leA:A -> A -> Prop
x:A
H:[x] = [] ++ [x]
Descl [] /\ Descl [x]
A:Set
leA:A -> A -> Prop
x:A
H:[x] = [x] ++ []
Descl [x] /\ Descl []
      +A:Set
leA:A -> A -> Prop
x:A
H:[x] = [] ++ [x]
Descl [] /\ Descl [x] split.A:Set
leA:A -> A -> Prop
x:A
H:[x] = [] ++ [x]
Descl []
A:Set
leA:A -> A -> Prop
x:A
H:[x] = [] ++ [x]
Descl [x]
        apply d_nil.A:Set
leA:A -> A -> Prop
x:A
H:[x] = [] ++ [x]
Descl [x]
        apply d_one.
      +A:Set
leA:A -> A -> Prop
x:A
H:[x] = [x] ++ []
Descl [x] /\ Descl [] split.A:Set
leA:A -> A -> Prop
x:A
H:[x] = [x] ++ []
Descl [x]
A:Set
leA:A -> A -> Prop
x:A
H:[x] = [x] ++ []
Descl []
        apply d_one.A:Set
leA:A -> A -> Prop
x:A
H:[x] = [x] ++ []
Descl []
        apply d_nil.
    -A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y1 : List,
l ++ [y] = x1 ++ y1 -> Descl x1 /\ Descl y1
x0, y0:List
H0:(l ++ [y]) ++ [x] = x0 ++ y0
Descl x0 /\ Descl y0 induction y0 using rev_ind in x0, H0 |- *.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0 ++ []
Descl x0 /\ Descl []
A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y1 : List,
l ++ [y] = x2 ++ y1 -> Descl x2 /\ Descl y1
x0:List
x1:A
y0:List
H0:(l ++ [y]) ++ [x] = x0 ++ y0 ++ [x1]
IHy0:forall x2 : List,
(l ++ [y]) ++ [x] = x2 ++ y0 ->
Descl x2 /\ Descl y0
Descl x0 /\ Descl (y0 ++ [x1])
      +A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0 ++ []
Descl x0 /\ Descl [] rewrite <- app_nil_end in H0.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0
Descl x0 /\ Descl []
        rewrite <- H0.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0
Descl ((l ++ [y]) ++ [x]) /\ Descl []
        split.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0
Descl ((l ++ [y]) ++ [x])
A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0
Descl []
        apply d_conc; auto with sets.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y0 : List,
l ++ [y] = x1 ++ y0 -> Descl x1 /\ Descl y0
x0:List
H0:(l ++ [y]) ++ [x] = x0
Descl []
        apply d_nil.
      +A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y1 : List,
l ++ [y] = x2 ++ y1 -> Descl x2 /\ Descl y1
x0:List
x1:A
y0:List
H0:(l ++ [y]) ++ [x] = x0 ++ y0 ++ [x1]
IHy0:forall x2 : List,
(l ++ [y]) ++ [x] = x2 ++ y0 ->
Descl x2 /\ Descl y0
Descl x0 /\ Descl (y0 ++ [x1]) induction y0 using rev_ind in x1, x0, H0 |- *.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl x0 /\ Descl ([] ++ [x1])
A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x3 y1 : List,
l ++ [y] = x3 ++ y1 -> Descl x3 /\ Descl y1
x0:List
x1, x2:A
y0:List
H0:(l ++ [y]) ++ [x] = x0 ++ (y0 ++ [x2]) ++ [x1]
IHy0:forall (x3 : List) (x4 : A),
(l ++ [y]) ++ [x] = x3 ++ y0 ++ [x4] ->
Descl x3 /\ Descl (y0 ++ [x4])
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x1])
        *A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl x0 /\ Descl ([] ++ [x1]) simpl.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl x0 /\ Descl [x1]
          split.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl x0
A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl [x1]
          apply app_inj_tail in H0 as (<-, _).A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x0 y0 : List,
l ++ [y] = x0 ++ y0 -> Descl x0 /\ Descl y0
x1:A
Descl (l ++ [y])
A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl [x1] assumption.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x2 y0 : List,
l ++ [y] = x2 ++ y0 -> Descl x2 /\ Descl y0
x0:List
x1:A
H0:(l ++ [y]) ++ [x] = x0 ++ [] ++ [x1]
Descl [x1]
          apply d_one.
        *A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x3 y1 : List,
l ++ [y] = x3 ++ y1 -> Descl x3 /\ Descl y1
x0:List
x1, x2:A
y0:List
H0:(l ++ [y]) ++ [x] = x0 ++ (y0 ++ [x2]) ++ [x1]
IHy0:forall (x3 : List) (x4 : A),
(l ++ [y]) ++ [x] = x3 ++ y0 ++ [x4] ->
Descl x3 /\ Descl (y0 ++ [x4])
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x1]) rewrite <- 2!app_assoc_reverse in H0.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x3 y1 : List,
l ++ [y] = x3 ++ y1 -> Descl x3 /\ Descl y1
x0:List
x1, x2:A
y0:List
H0:(l ++ [y]) ++ [x] = ((x0 ++ y0) ++ [x2]) ++ [x1]
IHy0:forall (x3 : List) (x4 : A),
(l ++ [y]) ++ [x] = x3 ++ y0 ++ [x4] ->
Descl x3 /\ Descl (y0 ++ [x4])
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x1])
          apply app_inj_tail in H0 as (H0, <-).A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y1 : List,
l ++ [y] = x1 ++ y1 -> Descl x1 /\ Descl y1
x0:List
x2:A
y0:List
H0:l ++ [y] = (x0 ++ y0) ++ [x2]
IHy0:forall (x1 : List) (x3 : A),
(l ++ [y]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x])
          pose proof H0 as H0'.A:Set
leA:A -> A -> Prop
x, y:A
l:List
H:clos_refl A leA x y
D:Descl (l ++ [y])
Hind:forall x1 y1 : List,
l ++ [y] = x1 ++ y1 -> Descl x1 /\ Descl y1
x0:List
x2:A
y0:List
H0:l ++ [y] = (x0 ++ y0) ++ [x2]
IHy0:forall (x1 : List) (x3 : A),
(l ++ [y]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0':l ++ [y] = (x0 ++ y0) ++ [x2]
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x])
          apply app_inj_tail in H0' as (_, ->).A:Set
leA:A -> A -> Prop
x:A
l:List
x2:A
Hind:forall x1 y : List,
l ++ [x2] = x1 ++ y -> Descl x1 /\ Descl y
D:Descl (l ++ [x2])
H:clos_refl A leA x x2
x0, y0:List
IHy0:forall (x1 : List) (x3 : A),
(l ++ [x2]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0:l ++ [x2] = (x0 ++ y0) ++ [x2]
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x])
          rewrite app_assoc_reverse in H0.A:Set
leA:A -> A -> Prop
x:A
l:List
x2:A
Hind:forall x1 y : List,
l ++ [x2] = x1 ++ y -> Descl x1 /\ Descl y
D:Descl (l ++ [x2])
H:clos_refl A leA x x2
x0, y0:List
IHy0:forall (x1 : List) (x3 : A),
(l ++ [x2]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0:l ++ [x2] = x0 ++ y0 ++ [x2]
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x])
          apply Hind in H0 as [].A:Set
leA:A -> A -> Prop
x:A
l:List
x2:A
Hind:forall x1 y : List,
l ++ [x2] = x1 ++ y -> Descl x1 /\ Descl y
D:Descl (l ++ [x2])
H:clos_refl A leA x x2
x0, y0:List
IHy0:forall (x1 : List) (x3 : A),
(l ++ [x2]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0:Descl x0
H1:Descl (y0 ++ [x2])
Descl x0 /\ Descl ((y0 ++ [x2]) ++ [x])
          split.A:Set
leA:A -> A -> Prop
x:A
l:List
x2:A
Hind:forall x1 y : List,
l ++ [x2] = x1 ++ y -> Descl x1 /\ Descl y
D:Descl (l ++ [x2])
H:clos_refl A leA x x2
x0, y0:List
IHy0:forall (x1 : List) (x3 : A),
(l ++ [x2]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0:Descl x0
H1:Descl (y0 ++ [x2])
Descl x0
A:Set
leA:A -> A -> Prop
x:A
l:List
x2:A
Hind:forall x1 y : List,
l ++ [x2] = x1 ++ y -> Descl x1 /\ Descl y
D:Descl (l ++ [x2])
H:clos_refl A leA x x2
x0, y0:List
IHy0:forall (x1 : List) (x3 : A),
(l ++ [x2]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0:Descl x0
H1:Descl (y0 ++ [x2])
Descl ((y0 ++ [x2]) ++ [x])
          assumption.A:Set
leA:A -> A -> Prop
x:A
l:List
x2:A
Hind:forall x1 y : List,
l ++ [x2] = x1 ++ y -> Descl x1 /\ Descl y
D:Descl (l ++ [x2])
H:clos_refl A leA x x2
x0, y0:List
IHy0:forall (x1 : List) (x3 : A),
(l ++ [x2]) ++ [x] = x1 ++ y0 ++ [x3] ->
Descl x1 /\ Descl (y0 ++ [x3])
H0:Descl x0
H1:Descl (y0 ++ [x2])
Descl ((y0 ++ [x2]) ++ [x])
          apply d_conc; auto with sets.
  Qed.



  Lemma dist_Desc_concat :
    forall x y : List, Descl (x ++ y) -> Descl x /\ Descl y.A:Set
leA:A -> A -> Prop
forall x y : List,
Descl (x ++ y) -> Descl x /\ Descl y
  Proof.A:Set
leA:A -> A -> Prop
forall x y : List,
Descl (x ++ y) -> Descl x /\ Descl y
    intros.A:Set
leA:A -> A -> Prop
x, y:List
H:Descl (x ++ y)
Descl x /\ Descl y
    apply (dist_aux (x ++ y) H x y); auto with sets.
  Qed.

  Lemma desc_end :
    forall (a b : A) (x : List),
      Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] -> clos_trans A leA a b.A:Set
leA:A -> A -> Prop
forall (a b : A) (x : List),
Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] ->
clos_trans A leA a b
  Proof.A:Set
leA:A -> A -> Prop
forall (a b : A) (x : List),
Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] ->
clos_trans A leA a b
    intros a b x.A:Set
leA:A -> A -> Prop
a, b:A
x:List
Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] ->
clos_trans A leA a b
    case x.A:Set
leA:A -> A -> Prop
a, b:A
x:List
Descl ([] ++ [a]) /\ ltl ([] ++ [a]) [b] ->
clos_trans A leA a b
A:Set
leA:A -> A -> Prop
a, b:A
x:List
forall (a0 : A) (l : List),
Descl ((a0 :: l) ++ [a]) /\ ltl ((a0 :: l) ++ [a]) [b] ->
clos_trans A leA a b
    simpl.A:Set
leA:A -> A -> Prop
a, b:A
x:List
Descl [a] /\ ltl [a] [b] -> clos_trans A leA a b
A:Set
leA:A -> A -> Prop
a, b:A
x:List
forall (a0 : A) (l : List),
Descl ((a0 :: l) ++ [a]) /\ ltl ((a0 :: l) ++ [a]) [b] ->
clos_trans A leA a b
    simple induction 1.A:Set
leA:A -> A -> Prop
a, b:A
x:List
H:Descl [a] /\ ltl [a] [b]
Descl [a] -> ltl [a] [b] -> clos_trans A leA a b
A:Set
leA:A -> A -> Prop
a, b:A
x:List
forall (a0 : A) (l : List),
Descl ((a0 :: l) ++ [a]) /\ ltl ((a0 :: l) ++ [a]) [b] ->
clos_trans A leA a b
    intros.A:Set
leA:A -> A -> Prop
a, b:A
x:List
H:Descl [a] /\ ltl [a] [b]
H0:Descl [a]
H1:ltl [a] [b]
clos_trans A leA a b
A:Set
leA:A -> A -> Prop
a, b:A
x:List
forall (a0 : A) (l : List),
Descl ((a0 :: l) ++ [a]) /\ ltl ((a0 :: l) ++ [a]) [b] ->
clos_trans A leA a b
    inversion H1; auto with sets.A:Set
leA:A -> A -> Prop
a, b:A
x:List
H:Descl [a] /\ ltl [a] [b]
H0:Descl [a]
H1:ltl [a] [b]
a0:A
x0, y:List
H3:ltl [] []
H2:a0 = a
H4:x0 = []
H5:a = b
H6:y = []
clos_trans A leA b b
A:Set
leA:A -> A -> Prop
a, b:A
x:List
forall (a0 : A) (l : List),
Descl ((a0 :: l) ++ [a]) /\ ltl ((a0 :: l) ++ [a]) [b] ->
clos_trans A leA a b
    inversion H3.A:Set
leA:A -> A -> Prop
a, b:A
x:List
forall (a0 : A) (l : List),
Descl ((a0 :: l) ++ [a]) /\ ltl ((a0 :: l) ++ [a]) [b] ->
clos_trans A leA a b

    simple induction 1.A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
Descl ((a0 :: l) ++ [a]) ->
ltl ((a0 :: l) ++ [a]) [b] -> clos_trans A leA a b
    generalize (app_comm_cons l [a] a0).A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
a0 :: l ++ [a] = (a0 :: l) ++ [a] ->
Descl ((a0 :: l) ++ [a]) ->
ltl ((a0 :: l) ++ [a]) [b] -> clos_trans A leA a b
    intros E; rewrite <- E; intros.A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
E:a0 :: l ++ [a] = (a0 :: l) ++ [a]
H0:Descl (a0 :: l ++ [a])
H1:ltl (a0 :: l ++ [a]) [b]
clos_trans A leA a b
    generalize (desc_tail l a a0 H0); intro.A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
E:a0 :: l ++ [a] = (a0 :: l) ++ [a]
H0:Descl (a0 :: l ++ [a])
H1:ltl (a0 :: l ++ [a]) [b]
H2:clos_refl_trans A leA a a0
clos_trans A leA a b
    inversion H1.A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
E:a0 :: l ++ [a] = (a0 :: l) ++ [a]
H0:Descl (a0 :: l ++ [a])
H1:ltl (a0 :: l ++ [a]) [b]
H2:clos_refl_trans A leA a a0
a1, b0:A
x0, y:List
H4:leA a0 b
H3:a1 = a0
H5:x0 = l ++ [a]
H6:b0 = b
H7:y = []
clos_trans A leA a b
A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
E:a0 :: l ++ [a] = (a0 :: l) ++ [a]
H0:Descl (a0 :: l ++ [a])
H1:ltl (a0 :: l ++ [a]) [b]
H2:clos_refl_trans A leA a a0
a1:A
x0, y:List
H4:ltl (l ++ [a]) []
H3:a1 = a0
H5:x0 = l ++ [a]
H6:a0 = b
H7:y = []
clos_trans A leA a b
    eapply clos_rt_t; [ eassumption | apply t_step; assumption ].A:Set
leA:A -> A -> Prop
a, b:A
x:List
a0:A
l:List
H:Descl ((a0 :: l) ++ [a]) /\
ltl ((a0 :: l) ++ [a]) [b]
E:a0 :: l ++ [a] = (a0 :: l) ++ [a]
H0:Descl (a0 :: l ++ [a])
H1:ltl (a0 :: l ++ [a]) [b]
H2:clos_refl_trans A leA a a0
a1:A
x0, y:List
H4:ltl (l ++ [a]) []
H3:a1 = a0
H5:x0 = l ++ [a]
H6:a0 = b
H7:y = []
clos_trans A leA a b

    inversion H4.
  Qed.




  Lemma ltl_unit :
    forall (x : List) (a b : A),
      Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b].A:Set
leA:A -> A -> Prop
forall (x : List) (a b : A),
Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b]
  Proof.A:Set
leA:A -> A -> Prop
forall (x : List) (a b : A),
Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b]
    intro.A:Set
leA:A -> A -> Prop
x:List
forall a b : A,
Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b]
    case x.A:Set
leA:A -> A -> Prop
x:List
forall a b : A,
Descl ([] ++ [a]) -> ltl ([] ++ [a]) [b] -> ltl [] [b]
A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List) (a0 b : A),
Descl ((a :: l) ++ [a0]) ->
ltl ((a :: l) ++ [a0]) [b] -> ltl (a :: l) [b]
    intros; apply (Lt_nil A leA).A:Set
leA:A -> A -> Prop
x:List
forall (a : A) (l : List) (a0 b : A),
Descl ((a :: l) ++ [a0]) ->
ltl ((a :: l) ++ [a0]) [b] -> ltl (a :: l) [b]

    simpl; intros.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
a0, b:A
H:Descl (a :: l ++ [a0])
H0:ltl (a :: l ++ [a0]) [b]
ltl (a :: l) [b]
    inversion_clear H0.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
a0, b:A
H:Descl (a :: l ++ [a0])
H1:leA a b
ltl (a :: l) [b]
A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
a0, b:A
H:Descl (a :: l ++ [a0])
H1:ltl (l ++ [a0]) []
ltl (b :: l) [b]
    apply (Lt_hd A leA a b); auto with sets.A:Set
leA:A -> A -> Prop
x:List
a:A
l:List
a0, b:A
H:Descl (a :: l ++ [a0])
H1:ltl (l ++ [a0]) []
ltl (b :: l) [b]

    inversion_clear H1.
  Qed.


  Lemma acc_app :
    forall (x1 x2 : List) (y1 : Descl (x1 ++ x2)),
      Acc Lex_Exp << x1 ++ x2, y1 >> ->
      forall (x : List) (y : Descl x),
        ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>.A:Set
leA:A -> A -> Prop
forall (x1 x2 : List) (y1 : Descl (x1 ++ x2)),
Acc Lex_Exp << x1 ++ x2, y1 >> ->
forall (x : List) (y : Descl x),
ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>
  Proof.A:Set
leA:A -> A -> Prop
forall (x1 x2 : List) (y1 : Descl (x1 ++ x2)),
Acc Lex_Exp << x1 ++ x2, y1 >> ->
forall (x : List) (y : Descl x),
ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>
    intros.A:Set
leA:A -> A -> Prop
x1, x2:List
y1:Descl (x1 ++ x2)
H:Acc Lex_Exp << x1 ++ x2, y1 >>
x:List
y:Descl x
H0:ltl x (x1 ++ x2)
Acc Lex_Exp << x, y >>
    apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).A:Set
leA:A -> A -> Prop
x1, x2:List
y1:Descl (x1 ++ x2)
H:Acc Lex_Exp << x1 ++ x2, y1 >>
x:List
y:Descl x
H0:ltl x (x1 ++ x2)
Acc Lex_Exp << x1 ++ x2, y1 >>
A:Set
leA:A -> A -> Prop
x1, x2:List
y1:Descl (x1 ++ x2)
H:Acc Lex_Exp << x1 ++ x2, y1 >>
x:List
y:Descl x
H0:ltl x (x1 ++ x2)
Lex_Exp << x, y >> << x1 ++ x2, y1 >>
    auto with sets.A:Set
leA:A -> A -> Prop
x1, x2:List
y1:Descl (x1 ++ x2)
H:Acc Lex_Exp << x1 ++ x2, y1 >>
x:List
y:Descl x
H0:ltl x (x1 ++ x2)
Lex_Exp << x, y >> << x1 ++ x2, y1 >>

    unfold lex_exp; simpl; auto with sets.
  Qed.


  Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.A:Set
leA:A -> A -> Prop
well_founded leA -> well_founded Lex_Exp
  Proof.A:Set
leA:A -> A -> Prop
well_founded leA -> well_founded Lex_Exp
    unfold well_founded at 2.A:Set
leA:A -> A -> Prop
well_founded leA -> forall a : Power, Acc Lex_Exp a
    simple induction a; intros x y.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
Acc Lex_Exp << x, y >>
    apply Acc_intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
forall y0 : Power,
Lex_Exp y0 << x, y >> -> Acc Lex_Exp y0
    simple induction y0.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
forall (x0 : List) (p : Descl x0),
Lex_Exp << x0, p >> << x, y >> ->
Acc Lex_Exp << x0, p >>
    unfold lex_exp at 1; simpl.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
forall (x0 : List) (p : Descl x0),
ltl x0 x -> Acc Lex_Exp << x0, p >>
    apply rev_ind with
      (A := A)
      (P := 
        fun x : List =>
        forall (x0 : List) (y : Descl x0),
          ltl x0 x -> Acc Lex_Exp << x0, y >>).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
forall (x0 : List) (y1 : Descl x0),
ltl x0 [] -> Acc Lex_Exp << x0, y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
forall (x0 : A) (l : List),
(forall (x1 : List) (y1 : Descl x1),
 ltl x1 l -> Acc Lex_Exp << x1, y1 >>) ->
forall (x1 : List) (y1 : Descl x1),
ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y1 >>
    intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:List
y1:Descl x0
H0:ltl x0 []
Acc Lex_Exp << x0, y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
forall (x0 : A) (l : List),
(forall (x1 : List) (y1 : Descl x1),
 ltl x1 l -> Acc Lex_Exp << x1, y1 >>) ->
forall (x1 : List) (y1 : Descl x1),
ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y1 >>
    inversion_clear H0.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
forall (x0 : A) (l : List),
(forall (x1 : List) (y1 : Descl x1),
 ltl x1 l -> Acc Lex_Exp << x1, y1 >>) ->
forall (x1 : List) (y1 : Descl x1),
ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y1 >>

    intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
forall l : List,
(forall (x1 : List) (y1 : Descl x1),
 ltl x1 l -> Acc Lex_Exp << x1, y1 >>) ->
forall (x1 : List) (y1 : Descl x1),
ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y1 >>
    generalize (well_founded_ind (wf_clos_trans A leA H)).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
(forall P : A -> Prop,
 (forall x1 : A,
  (forall y1 : A, clos_trans A leA y1 x1 -> P y1) ->
  P x1) -> forall a0 : A, P a0) ->
forall l : List,
(forall (x1 : List) (y1 : Descl x1),
 ltl x1 l -> Acc Lex_Exp << x1, y1 >>) ->
forall (x1 : List) (y1 : Descl x1),
ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y1 >>
    intros GR.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x1 : A,
 (forall y1 : A, clos_trans A leA y1 x1 -> P y1) ->
 P x1) -> forall a0 : A, P a0
forall l : List,
(forall (x1 : List) (y1 : Descl x1),
 ltl x1 l -> Acc Lex_Exp << x1, y1 >>) ->
forall (x1 : List) (y1 : Descl x1),
ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y1 >>
    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 ++ [x0]) -> Acc Lex_Exp << x1, y >>).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x1 : A,
 (forall y1 : A, clos_trans A leA y1 x1 -> P y1) ->
 P x1) -> forall a0 : A, P a0
forall x1 : A,
(forall y1 : A,
 clos_trans A leA y1 x1 ->
 forall l : List,
 (forall (x2 : List) (y2 : Descl x2),
  ltl x2 l -> Acc Lex_Exp << x2, y2 >>) ->
 forall (x2 : List) (y2 : Descl x2),
 ltl x2 (l ++ [y1]) -> Acc Lex_Exp << x2, y2 >>) ->
forall l : List,
(forall (x2 : List) (y1 : Descl x2),
 ltl x2 l -> Acc Lex_Exp << x2, y1 >>) ->
forall (x2 : List) (y1 : Descl x2),
ltl x2 (l ++ [x1]) -> Acc Lex_Exp << x2, y1 >>
    intro; intros HInd; intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x3 : A,
 (forall y2 : A, clos_trans A leA y2 x3 -> P y2) ->
 P x3) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x3 : List) (y3 : Descl x3),
 ltl x3 l0 -> Acc Lex_Exp << x3, y3 >>) ->
forall (x3 : List) (y3 : Descl x3),
ltl x3 (l0 ++ [y2]) -> Acc Lex_Exp << x3, y3 >>
l:List
H0:forall (x3 : List) (y2 : Descl x3),
ltl x3 l -> Acc Lex_Exp << x3, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
Acc Lex_Exp << x2, y1 >>
    generalize (right_prefix x2 l [x1] H1).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x3 : A,
 (forall y2 : A, clos_trans A leA y2 x3 -> P y2) ->
 P x3) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x3 : List) (y3 : Descl x3),
 ltl x3 l0 -> Acc Lex_Exp << x3, y3 >>) ->
forall (x3 : List) (y3 : Descl x3),
ltl x3 (l0 ++ [y2]) -> Acc Lex_Exp << x3, y3 >>
l:List
H0:forall (x3 : List) (y2 : Descl x3),
ltl x3 l -> Acc Lex_Exp << x3, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1]) ->
Acc Lex_Exp << x2, y1 >>
    simple induction 1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x3 : A,
 (forall y2 : A, clos_trans A leA y2 x3 -> P y2) ->
 P x3) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x3 : List) (y3 : Descl x3),
 ltl x3 l0 -> Acc Lex_Exp << x3, y3 >>) ->
forall (x3 : List) (y3 : Descl x3),
ltl x3 (l0 ++ [y2]) -> Acc Lex_Exp << x3, y3 >>
l:List
H0:forall (x3 : List) (y2 : Descl x3),
ltl x3 l -> Acc Lex_Exp << x3, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
H2:ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1])
ltl x2 l -> Acc Lex_Exp << x2, y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x3 : A,
 (forall y2 : A, clos_trans A leA y2 x3 -> P y2) ->
 P x3) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x3 : List) (y3 : Descl x3),
 ltl x3 l0 -> Acc Lex_Exp << x3, y3 >>) ->
forall (x3 : List) (y3 : Descl x3),
ltl x3 (l0 ++ [y2]) -> Acc Lex_Exp << x3, y3 >>
l:List
H0:forall (x3 : List) (y2 : Descl x3),
ltl x3 l -> Acc Lex_Exp << x3, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
H2:ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1])
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1]) ->
Acc Lex_Exp << x2, y1 >>
    intro; apply (H0 x2 y1 H3).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x3 : A,
 (forall y2 : A, clos_trans A leA y2 x3 -> P y2) ->
 P x3) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x3 : List) (y3 : Descl x3),
 ltl x3 l0 -> Acc Lex_Exp << x3, y3 >>) ->
forall (x3 : List) (y3 : Descl x3),
ltl x3 (l0 ++ [y2]) -> Acc Lex_Exp << x3, y3 >>
l:List
H0:forall (x3 : List) (y2 : Descl x3),
ltl x3 l -> Acc Lex_Exp << x3, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
H2:ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1])
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1]) ->
Acc Lex_Exp << x2, y1 >>

    simple induction 1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x3 : A,
 (forall y2 : A, clos_trans A leA y2 x3 -> P y2) ->
 P x3) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x3 : List) (y3 : Descl x3),
 ltl x3 l0 -> Acc Lex_Exp << x3, y3 >>) ->
forall (x3 : List) (y3 : Descl x3),
ltl x3 (l0 ++ [y2]) -> Acc Lex_Exp << x3, y3 >>
l:List
H0:forall (x3 : List) (y2 : Descl x3),
ltl x3 l -> Acc Lex_Exp << x3, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
H2:ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
forall x3 : List,
x2 = l ++ x3 /\ ltl x3 [x1] ->
Acc Lex_Exp << x2, y1 >>
    intro; simple induction 1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
H2:ltl x2 l \/
(exists y' : List, x2 = l ++ y' /\ ltl y' [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H4:x2 = l ++ x3 /\ ltl x3 [x1]
x2 = l ++ x3 ->
ltl x3 [x1] -> Acc Lex_Exp << x2, y1 >>
    clear H4 H2.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
y1:Descl x2
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
x2 = l ++ x3 ->
ltl x3 [x1] -> Acc Lex_Exp << x2, y1 >>
    intro; generalize y1; clear y1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall y1 : Descl x2,
ltl x3 [x1] -> Acc Lex_Exp << x2, y1 >>
    rewrite H2.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall y1 : Descl (l ++ x3),
ltl x3 [x1] -> Acc Lex_Exp << l ++ x3, y1 >>
    apply rev_ind with
      (A := A)
      (P := 
        fun x3 : List =>
        forall y1 : Descl (l ++ x3),
          ltl x3 [x1] -> Acc Lex_Exp << l ++ x3, y1 >>).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall y1 : Descl (l ++ []),
ltl [] [x1] -> Acc Lex_Exp << l ++ [], y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
y1:Descl (l ++ [])
H4:ltl [] [x1]
Acc Lex_Exp << l ++ [], y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    generalize (app_nil_end l); intros Heq.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
y1:Descl (l ++ [])
H4:ltl [] [x1]
Heq:l = l ++ []
Acc Lex_Exp << l ++ [], y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    generalize y1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
y1:Descl (l ++ [])
H4:ltl [] [x1]
Heq:l = l ++ []
forall y2 : Descl (l ++ []),
Acc Lex_Exp << l ++ [], y2 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    clear y1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
forall y1 : Descl (l ++ []),
Acc Lex_Exp << l ++ [], y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    rewrite <- Heq.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
forall y1 : Descl l, Acc Lex_Exp << l, y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
y1:Descl l
Acc Lex_Exp << l, y1 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    apply Acc_intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y2 : A, clos_trans A leA y2 x4 -> P y2) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l0 : List,
(forall (x4 : List) (y3 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y3 >>) ->
forall (x4 : List) (y3 : Descl x4),
ltl x4 (l0 ++ [y2]) -> Acc Lex_Exp << x4, y3 >>
l:List
H0:forall (x4 : List) (y2 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
y1:Descl l
forall y2 : Power,
Lex_Exp y2 << l, y1 >> -> Acc Lex_Exp y2
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    simple induction y2.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y3 : A, clos_trans A leA y3 x4 -> P y3) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l0 : List,
(forall (x4 : List) (y4 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y4 >>) ->
forall (x4 : List) (y4 : Descl x4),
ltl x4 (l0 ++ [y3]) -> Acc Lex_Exp << x4, y4 >>
l:List
H0:forall (x4 : List) (y3 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
y1:Descl l
y2:Power
forall (x4 : List) (p : Descl x4),
Lex_Exp << x4, p >> << l, y1 >> ->
Acc Lex_Exp << x4, p >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    unfold lex_exp at 1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y3 : A, clos_trans A leA y3 x4 -> P y3) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l0 : List,
(forall (x4 : List) (y4 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y4 >>) ->
forall (x4 : List) (y4 : Descl x4),
ltl x4 (l0 ++ [y3]) -> Acc Lex_Exp << x4, y4 >>
l:List
H0:forall (x4 : List) (y3 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
y1:Descl l
y2:Power
forall (x4 : List) (p : Descl x4),
ltl (proj1_sig << x4, p >>) (proj1_sig << l, y1 >>) ->
Acc Lex_Exp << x4, p >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    simpl; intros x4 y3.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y4 : A, clos_trans A leA y4 x5 -> P y4) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y4 : A,
clos_trans A leA y4 x1 ->
forall l0 : List,
(forall (x5 : List) (y5 : Descl x5),
 ltl x5 l0 -> Acc Lex_Exp << x5, y5 >>) ->
forall (x5 : List) (y5 : Descl x5),
ltl x5 (l0 ++ [y4]) -> Acc Lex_Exp << x5, y5 >>
l:List
H0:forall (x5 : List) (y4 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y4 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
y1:Descl l
y2:Power
x4:List
y3:Descl x4
ltl x4 l -> Acc Lex_Exp << x4, y3 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >> intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y4 : A, clos_trans A leA y4 x5 -> P y4) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y4 : A,
clos_trans A leA y4 x1 ->
forall l0 : List,
(forall (x5 : List) (y5 : Descl x5),
 ltl x5 l0 -> Acc Lex_Exp << x5, y5 >>) ->
forall (x5 : List) (y5 : Descl x5),
ltl x5 (l0 ++ [y4]) -> Acc Lex_Exp << x5, y5 >>
l:List
H0:forall (x5 : List) (y4 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y4 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
H4:ltl [] [x1]
Heq:l = l ++ []
y1:Descl l
y2:Power
x4:List
y3:Descl x4
H5:ltl x4 l
Acc Lex_Exp << x4, y3 >>
A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    apply (H0 x4 y3); auto with sets.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x4 : A,
 (forall y1 : A, clos_trans A leA y1 x4 -> P y1) ->
 P x4) -> forall a0 : A, P a0
x1:A
HInd:forall y1 : A,
clos_trans A leA y1 x1 ->
forall l0 : List,
(forall (x4 : List) (y2 : Descl x4),
 ltl x4 l0 -> Acc Lex_Exp << x4, y2 >>) ->
forall (x4 : List) (y2 : Descl x4),
ltl x4 (l0 ++ [y1]) -> Acc Lex_Exp << x4, y2 >>
l:List
H0:forall (x4 : List) (y1 : Descl x4),
ltl x4 l -> Acc Lex_Exp << x4, y1 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
forall (x4 : A) (l0 : List),
(forall y1 : Descl (l ++ l0),
 ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y1 >>) ->
forall y1 : Descl (l ++ l0 ++ [x4]),
ltl (l0 ++ [x4]) [x1] ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>

    intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y2 : A, clos_trans A leA y2 x5 -> P y2) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l1 : List,
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 (l1 ++ [y2]) -> Acc Lex_Exp << x5, y3 >>
l:List
H0:forall (x5 : List) (y2 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y2 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y2 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    generalize (dist_Desc_concat l (l0 ++ [x4]) y1).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y2 : A, clos_trans A leA y2 x5 -> P y2) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l1 : List,
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 (l1 ++ [y2]) -> Acc Lex_Exp << x5, y3 >>
l:List
H0:forall (x5 : List) (y2 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y2 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y2 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
Descl l /\ Descl (l0 ++ [x4]) ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    simple induction 1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y2 : A, clos_trans A leA y2 x5 -> P y2) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l1 : List,
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 (l1 ++ [y2]) -> Acc Lex_Exp << x5, y3 >>
l:List
H0:forall (x5 : List) (y2 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y2 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y2 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
Descl l ->
Descl (l0 ++ [x4]) ->
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y2 : A, clos_trans A leA y2 x5 -> P y2) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l1 : List,
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 (l1 ++ [y2]) -> Acc Lex_Exp << x5, y3 >>
l:List
H0:forall (x5 : List) (y2 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y2 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y2 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    generalize (desc_end x4 x1 l0 (conj H8 H5)); intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y2 : A, clos_trans A leA y2 x5 -> P y2) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l1 : List,
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 (l1 ++ [y2]) -> Acc Lex_Exp << x5, y3 >>
l:List
H0:forall (x5 : List) (y2 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y2 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y2 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
Acc Lex_Exp << l ++ l0 ++ [x4], y1 >>
    generalize y1.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y2 : A, clos_trans A leA y2 x5 -> P y2) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y2 : A,
clos_trans A leA y2 x1 ->
forall l1 : List,
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 (l1 ++ [y2]) -> Acc Lex_Exp << x5, y3 >>
l:List
H0:forall (x5 : List) (y2 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y2 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y2 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y2 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
forall y2 : Descl (l ++ l0 ++ [x4]),
Acc Lex_Exp << l ++ l0 ++ [x4], y2 >>
    rewrite <- (app_assoc_reverse l l0 [x4]); intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (HInd x4 H9 (l ++ l0)); intros HInd2.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (ltl_unit l0 x4 x1 H8 H5); intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (dist_Desc_concat (l ++ l0) [x4] y2).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
Descl (l ++ l0) /\ Descl [x4] ->
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    simple induction 1; intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (H4 H12 H10); intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (Acc_inv H14).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
(forall y3 : Power,
 Lex_Exp y3 << l ++ l0, H12 >> -> Acc Lex_Exp y3) ->
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (acc_app l l0 H12 H14).A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
(forall y3 : Power,
 Lex_Exp y3 << l ++ l0, H12 >> -> Acc Lex_Exp y3) ->
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    intros f g.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
f:forall (x5 : List) (y3 : Descl x5),
ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>
g:forall y3 : Power,
Lex_Exp y3 << l ++ l0, H12 >> -> Acc Lex_Exp y3
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    generalize (HInd2 f); intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
f:forall (x5 : List) (y3 : Descl x5),
ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>
g:forall y3 : Power,
Lex_Exp y3 << l ++ l0, H12 >> -> Acc Lex_Exp y3
H15:forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
Acc Lex_Exp << (l ++ l0) ++ [x4], y2 >>
    apply Acc_intro.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y3 : A, clos_trans A leA y3 x5 -> P y3) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y3 : A,
clos_trans A leA y3 x1 ->
forall l1 : List,
(forall (x5 : List) (y4 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 (l1 ++ [y3]) -> Acc Lex_Exp << x5, y4 >>
l:List
H0:forall (x5 : List) (y3 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y3 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y3 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y3 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y3 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>) ->
forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
f:forall (x5 : List) (y3 : Descl x5),
ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y3 >>
g:forall y3 : Power,
Lex_Exp y3 << l ++ l0, H12 >> -> Acc Lex_Exp y3
H15:forall (x5 : List) (y3 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y3 >>
forall y3 : Power,
Lex_Exp y3 << (l ++ l0) ++ [x4], y2 >> ->
Acc Lex_Exp y3
    simple induction y3.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x5 : A,
 (forall y4 : A, clos_trans A leA y4 x5 -> P y4) ->
 P x5) -> forall a0 : A, P a0
x1:A
HInd:forall y4 : A,
clos_trans A leA y4 x1 ->
forall l1 : List,
(forall (x5 : List) (y5 : Descl x5),
 ltl x5 l1 -> Acc Lex_Exp << x5, y5 >>) ->
forall (x5 : List) (y5 : Descl x5),
ltl x5 (l1 ++ [y4]) -> Acc Lex_Exp << x5, y5 >>
l:List
H0:forall (x5 : List) (y4 : Descl x5),
ltl x5 l -> Acc Lex_Exp << x5, y4 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y4 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y4 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x5 : List) (y4 : Descl x5),
 ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y4 >>) ->
forall (x5 : List) (y4 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y4 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
f:forall (x5 : List) (y4 : Descl x5),
ltl x5 (l ++ l0) -> Acc Lex_Exp << x5, y4 >>
g:forall y4 : Power,
Lex_Exp y4 << l ++ l0, H12 >> -> Acc Lex_Exp y4
H15:forall (x5 : List) (y4 : Descl x5),
ltl x5 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x5, y4 >>
y3:Power
forall (x5 : List) (p : Descl x5),
Lex_Exp << x5, p >> << (l ++ l0) ++ [x4], y2 >> ->
Acc Lex_Exp << x5, p >>
    unfold lex_exp at 1; simpl; intros.A:Set
leA:A -> A -> Prop
H:well_founded leA
a:Power
x:List
y:Descl x
y0:Power
x0:A
GR:forall P : A -> Prop,
(forall x6 : A,
 (forall y4 : A, clos_trans A leA y4 x6 -> P y4) ->
 P x6) -> forall a0 : A, P a0
x1:A
HInd:forall y4 : A,
clos_trans A leA y4 x1 ->
forall l1 : List,
(forall (x6 : List) (y5 : Descl x6),
 ltl x6 l1 -> Acc Lex_Exp << x6, y5 >>) ->
forall (x6 : List) (y5 : Descl x6),
ltl x6 (l1 ++ [y4]) -> Acc Lex_Exp << x6, y5 >>
l:List
H0:forall (x6 : List) (y4 : Descl x6),
ltl x6 l -> Acc Lex_Exp << x6, y4 >>
x2:List
H1:ltl x2 (l ++ [x1])
H3:exists y' : List, x2 = l ++ y' /\ ltl y' [x1]
x3:List
H2:x2 = l ++ x3
x4:A
l0:List
H4:forall y4 : Descl (l ++ l0),
ltl l0 [x1] -> Acc Lex_Exp << l ++ l0, y4 >>
y1:Descl (l ++ l0 ++ [x4])
H5:ltl (l0 ++ [x4]) [x1]
H6:Descl l /\ Descl (l0 ++ [x4])
H7:Descl l
H8:Descl (l0 ++ [x4])
H9:clos_trans A leA x4 x1
y2:Descl ((l ++ l0) ++ [x4])
HInd2:(forall (x6 : List) (y4 : Descl x6),
 ltl x6 (l ++ l0) -> Acc Lex_Exp << x6, y4 >>) ->
forall (x6 : List) (y4 : Descl x6),
ltl x6 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x6, y4 >>
H10:ltl l0 [x1]
H11:Descl (l ++ l0) /\ Descl [x4]
H12:Descl (l ++ l0)
H13:Descl [x4]
H14:Acc Lex_Exp << l ++ l0, H12 >>
f:forall (x6 : List) (y4 : Descl x6),
ltl x6 (l ++ l0) -> Acc Lex_Exp << x6, y4 >>
g:forall y4 : Power,
Lex_Exp y4 << l ++ l0, H12 >> -> Acc Lex_Exp y4
H15:forall (x6 : List) (y4 : Descl x6),
ltl x6 ((l ++ l0) ++ [x4]) ->
Acc Lex_Exp << x6, y4 >>
y3:Power
x5:List
p:Descl x5
H16:ltl x5 ((l ++ l0) ++ [x4])
Acc Lex_Exp << x5, p >>
    apply H15; auto with sets.
  Qed.


End Wf_Lexicographic_Exponentiation.