(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                              inversionSL.v                               *)
(****************************************************************************)

(*****************************************************************************)
(*                                                                           *)
(*      Meta-theory of the explicit substitution calculus lambda-env         *)
(*      Amokrane Saibi                                                       *)
(*                                                                           *)
(*      September 1993                                                       *)
(*                                                                           *)
(*****************************************************************************)


                       (* Inversion de sigma_lift (relSL) *)
Require Import sur_les_relations.
Require Import TS.
Require Import sigma_lift.

(*****************
Definition e_invSL:=[b:wsort][M:(TS b)][N:(TS b)]
(<[b:wsort]Prop>Case M of
 (* var *) [n:nat] False
 (* app *) [M1,M2:terms]
           (<[b:wsort]Prop>Case N of
            (* var *) [n:nat]False
            (* app *) [N1,N2:terms]
                      ((relSL M1 N1) /\ (M2=N2)) 
                   \/ ((M1=N1) /\ (relSL M2 N2))
            (* lam *) [N1:terms]False 
            (* env *) [N1:terms][N2:sub_explicits]False
            (* id  *) False
            (*  |  *) False
            (*  .  *) [N1:terms][N2:sub_explicits]False
            (*  o  *) [N1,N2:sub_explicits]False
            (* ||  *) [N1:sub_explicits]False
            (*  X  *) [n:nat]False
            (*  x  *) [n:nat]False  end)
 (* lam *) [M1:terms]
           (<[b:wsort]Prop>Case N of
            (* var *) [n:nat]False
            (* app *) [N1,N2:terms]False 
            (* lam *) [N1:terms](relSL M1 N1)
            (* env *) [N1:terms][N2:sub_explicits]False
            (* id  *) False
            (*  |  *) False
            (*  .  *) [N1:terms][N2:sub_explicits]False
            (*  o  *) [N1,N2:sub_explicits]False
            (* ||  *) [N1:sub_explicits]False
            (*  X  *) [n:nat]False
            (*  x  *) [n:nat]False  end)
 (* env *) [M1:terms][M2:sub_explicits]
           (<[b:wsort]Prop>Case N of
            (* var *) [n:nat] 
                 (Ex( ([m:nat] (M1=(var m)) /\ (n=(S m)) /\ (M2=shift) )))
             \/  (Ex( ([s:sub_explicits] (M1=(var O)) /\
                                  (M2=(lift s)) /\ (n=O) )))
             \/  (Ex( ([s:sub_explicits] (M1=(var O)) /\
                            (M2=(cons (var n) s)) )))
             \/ ((M1=(var n)) /\ (M2=id))
            (* app *) [N1,N2:terms]
                (Ex( ([a:terms] (Ex( ([b:terms] (M1=(app a b))
                    /\ (N1=(env a M2)) /\ (N2=(env b M2)) ))) )))
             \/ (Ex( ([s:sub_explicits] (M1=(var O)) /\
                            (M2=(cons (app N1 N2) s)) )))
             \/ ((M1=(app N1 N2)) /\ (M2=id)) 
            (* lam *) [N1:terms]
                (Ex( ([a:terms] (M1=(lambda a))
                                 /\ (N1=(env a (lift M2))) )))
             \/ (Ex( ([s:sub_explicits] (M1=(var O)) /\
                            (M2=(cons (lambda N1) s)) )))
             \/ ((M1=(lambda N1)) /\ (M2=id) )
            (* env *) [N1:terms][N2:sub_explicits]
                (Ex( ([s:sub_explicits] (M1=(env N1 s)) /\
                            (N2=(comp s M2)) )))   
             \/ (Ex( ([n:nat] (M1=(var n)) /\
                       (M2=(comp shift N2)) /\ (N1=(var (S n))) )))
             \/ (Ex( ([s:sub_explicits] (M1=(var O)) /\
                               (M2=(cons (env N1 N2) s)) )))
             \/ (Ex( ([s:sub_explicits] (M1=(var O)) /\
                        (M2=(comp (lift s) N2)) /\ (N1=(var O)) )))
             \/ (Ex( ([n:nat] (Ex( ([a:terms] (M1=(var (S n))) /\
                        (M2=(cons a N2)) /\ (N1=(var n)) ))) )))
             \/ (Ex( ([n:nat] (Ex( ([s:sub_explicits]
                   (M1=(var (S n))) /\ (M2=(lift s)) /\
                   (N1=(var n)) /\ (N2=(comp s shift)) ))) )))
             \/ (Ex( ([n:nat] (Ex( ([s:sub_explicits]
                  (Ex( ([t:sub_explicits] (M1=(var (S n))) /\
                  (M2=(comp (lift s) t)) /\ (N1=(var n)) /\
                  (N2=(comp s (comp shift t))) ))) ))) )))
             \/ ((M1=(env N1 N2)) /\ (M2=id))                  
             \/ ((relSL M1 N1) /\ (M2=N2))
             \/ ((M1=N1) /\ (relSL M2 N2))
            (* id  *) False
            (*  |  *) False
            (*  .  *) [N1:terms][N2:sub_explicits]False
            (*  o  *) [N1,N2:sub_explicits]False
            (* ||  *) [N1:sub_explicits]False
            (*  X  *) [n:nat]
             (Ex( ([s:sub_explicits] (M1=(var O)) /\
                            (M2=(cons (meta_X n) s)) )))
             \/ ((M1=(meta_X n)) /\ (M2=id))
            (*  x  *) [n:nat]False  end)
 (* id  *) False
 (*  |  *) False 
 (*  .  *) [M1:terms][M2:sub_explicits]
           (<[b:wsort]Prop>Case N of
            (* var *) [n:nat]False
            (* app *) [N1,N2:terms]False 
            (* lam *) [N1:terms]False 
            (* env *) [N1:terms][N2:sub_explicits]False
            (* id  *) False
            (*  |  *) False
            (*  .  *) [N1:terms][N2:sub_explicits]
                      ((relSL M1 N1) /\ (M2=N2))
                      \/  ((M1=N1) /\ (relSL M2 N2))
            (*  o  *) [N1,N2:sub_explicits]False
            (* ||  *) [N1:sub_explicits]False
            (*  X  *) [n:nat]False
            (*  x  *) [n:nat]False  end)
 (*  o  *) [M1,M2:sub_explicits]
           (<[b:wsort]Prop>Case N of
            (* var *) [n:nat]False
            (* app *) [N1,N2:terms]False 
            (* lam *) [N1:terms]False
            (* env *) [N1:terms][N2:sub_explicits]False
            (* id  *) (Ex( ([a:terms] (M1=shift) /\
                           (M2=(cons a id)) )))
                   \/ ((M1=id) /\ (M2=id))
            (*  |  *) (Ex( ([a:terms] (M1=shift) /\
                        (M2=(cons a shift)) )))
                   \/ ((M1=id) /\ (M2=shift))
                   \/ ((M1=shift) /\ (M2=id))
            (*  .  *) [N1:terms][N2:sub_explicits]
                  (Ex( ([a:terms](Ex( ([s:sub_explicits]
                     (M1=(cons a s)) /\ (N1=(env a M2)) /\
                     (N2=(comp s M2)) ))) )))
               \/ (Ex( ([a:terms] (M1=shift) /\
                        (M2=(cons a (cons N1 N2))) )))
               \/ (Ex( ([s:sub_explicits]
                     (Ex( ([t:sub_explicits] (M1=(lift s)) /\ (M2=(cons N1 t)) 
                         /\ (N2=(comp s t)) ))) )))
               \/ ((M1=id) /\ (M2=(cons N1 N2)))
               \/ ((M1=(cons N1 N2)) /\ (M2=id))
            (*  o  *) [N1,N2:sub_explicits]
                 (Ex( ([t:sub_explicits]
                   (M1=(comp N1 t)) /\ (N2=(comp t M2)) )))
              \/ (Ex( ([a:terms] (M1=shift) /\ (M2=(cons a (comp N1 N2))) )))
              \/ ((M1=shift) /\ (M2=(lift N1)) /\ (N2=shift))
              \/ (Ex( ([t:sub_explicits] (M1=shift) /\
                   (M2=(comp (lift N1) t)) /\ (N2=(comp shift t)) )))
              \/ (Ex( ([s:sub_explicits] 
                 (Ex( ([t:sub_explicits] (M1=(lift s)) /\
                    (M2=(comp (lift t) N2)) /\ (N1=(lift (comp s t)))))))))
              \/ ((M1=id) /\ (M2=(comp N1 N2)))
              \/ ((M1=(comp N1 N2)) /\ (M2=id))
              \/ ((relSL M1 N1) /\ (M2=N2))
              \/ ((M1=N1) /\ (relSL M2 N2)) 
            (* ||  *) [N1:sub_explicits]
                 (Ex( ([a:terms] (M1=shift) /\ (M2=(cons a (lift N1))))))
              \/ (Ex( ([s:sub_explicits] 
                 (Ex( ([t:sub_explicits] (M1=(lift s)) /\
                 (M2=(lift t)) /\ (N1=(comp s t)) ))) )))
              \/ ((M1=id) /\ (M2=(lift N1)))
              \/ ((M1=(lift N1)) /\ (M2=id))
            (*  X  *) [n:nat]False
            (*  x  *) [n:nat] 
                 (Ex( ([a:terms] (M1=shift) /\ (M2=(cons a (meta_x n))))))
                   \/ ((M1=id) /\ (M2=(meta_x n)))
                   \/ ((M1=(meta_x n)) /\ (M2=id))  end)
 (* ||  *) [M1:sub_explicits]
           (<[b:wsort]Prop>Case N of
            (* var *) [n:nat]False
            (* app *) [N1,N2:terms]False 
            (* lam *) [N1:terms]False
            (* env *) [N1:terms][N2:sub_explicits]False
            (* id  *) (M1=id)
            (*  |  *) False
            (*  .  *) [N1:terms][N2:sub_explicits]False
            (*  o  *) [N1,N2:sub_explicits]False
            (* ||  *) [N1:sub_explicits](relSL M1 N1)
            (*  X  *) [n:nat]False
            (*  x  *) [n:nat]False end)
  (*  X  *) [n:nat]False
  (*  x  *) [n:nat]False  end). 

****************)

Definition e_invSL (b : wsort) (M N : TS b) :=
  match M, N with
  | lift M1, id => M1 = id
  | lift M1, lift N1 => e_relSL _ M1 N1
  | lambda M1, lambda N1 => e_relSL _ M1 N1
  | app M1 M2, app N1 N2 =>
      e_relSL _ M1 N1 /\ M2 = N2 \/ M1 = N1 /\ e_relSL _ M2 N2
  | env M1 M2, var n as V =>
      (exists m : nat, M1 = var m /\ n = S m /\ M2 = shift) \/
      (exists s : sub_explicits, M1 = var 0 /\ M2 = lift s /\ n = 0) \/
      (exists s : sub_explicits, M1 = var 0 /\ M2 = cons V s) \/
      M1 = V /\ M2 = id
  | env M1 M2, app N1 N2 as A =>
      (exists a : terms,
         (exists b : terms, M1 = app a b /\ N1 = env a M2 /\ N2 = env b M2)) \/
      (exists s : sub_explicits, M1 = var 0 /\ M2 = cons A s) \/
      M1 = A /\ M2 = id
  | env M1 M2, lambda N1 as L =>
      (exists a : terms, M1 = lambda a /\ N1 = env a (lift M2)) \/
      (exists s : sub_explicits, M1 = var 0 /\ M2 = cons L s) \/
      M1 = L /\ M2 = id
  | env M1 M2, env N1 N2 as E =>
      (exists s : sub_explicits, M1 = env N1 s /\ N2 = comp s M2) \/
      (exists n : nat, M1 = var n /\ M2 = comp shift N2 /\ N1 = var (S n)) \/
      (exists s : sub_explicits, M1 = var 0 /\ M2 = cons E s) \/
      (exists s : sub_explicits,
         M1 = var 0 /\ M2 = comp (lift s) N2 /\ N1 = var 0) \/
      (exists n : nat,
         (exists a : terms, M1 = var (S n) /\ M2 = cons a N2 /\ N1 = var n)) \/
      (exists n : nat,
         (exists s : sub_explicits,
            M1 = var (S n) /\ M2 = lift s /\ N1 = var n /\ N2 = comp s shift)) \/
      (exists n : nat,
         (exists s : sub_explicits,
            (exists t : sub_explicits,
               M1 = var (S n) /\
               M2 = comp (lift s) t /\
               N1 = var n /\ N2 = comp s (comp shift t)))) \/
      M1 = E /\ M2 = id \/
      e_relSL _ M1 N1 /\ M2 = N2 \/ M1 = N1 /\ e_relSL _ M2 N2
  | env M1 M2, meta_X n =>
      (exists s : sub_explicits, M1 = var 0 /\ M2 = cons (meta_X n) s) \/
      M1 = meta_X n /\ M2 = id
  | cons M1 M2, cons N1 N2 =>
      e_relSL _ M1 N1 /\ M2 = N2 \/ M1 = N1 /\ e_relSL _ M2 N2
  | comp M1 M2, id =>
      (exists a : terms, M1 = shift /\ M2 = cons a id) \/ M1 = id /\ M2 = id
  | comp M1 M2, shift =>
      (exists a : terms, M1 = shift /\ M2 = cons a shift) \/
      M1 = id /\ M2 = shift \/ M1 = shift /\ M2 = id
  | comp M1 M2, cons N1 N2 as C =>
      (exists a : terms,
         (exists s : sub_explicits,
            M1 = cons a s /\ N1 = env a M2 /\ N2 = comp s M2)) \/
      (exists a : terms, M1 = shift /\ M2 = cons a C) \/
      (exists s : sub_explicits,
         (exists t : sub_explicits,
            M1 = lift s /\ M2 = cons N1 t /\ N2 = comp s t)) \/
      M1 = id /\ M2 = C \/ M1 = C /\ M2 = id
  | comp M1 M2, comp N1 N2 =>
      (exists t : sub_explicits, M1 = comp N1 t /\ N2 = comp t M2) \/
      (exists a : terms, M1 = shift /\ M2 = cons a (comp N1 N2)) \/
      M1 = shift /\ M2 = lift N1 /\ N2 = shift \/
      (exists t : sub_explicits,
         M1 = shift /\ M2 = comp (lift N1) t /\ N2 = comp shift t) \/
      (exists s : sub_explicits,
         (exists t : sub_explicits,
            M1 = lift s /\ M2 = comp (lift t) N2 /\ N1 = lift (comp s t))) \/
      M1 = id /\ M2 = comp N1 N2 \/
      M1 = comp N1 N2 /\ M2 = id \/
      e_relSL _ M1 N1 /\ M2 = N2 \/ M1 = N1 /\ e_relSL _ M2 N2
  | comp M1 M2, lift N1 as L =>
      (exists a : terms, M1 = shift /\ M2 = cons a L) \/
      (exists s : sub_explicits,
         (exists t : sub_explicits,
            M1 = lift s /\ M2 = lift t /\ N1 = comp s t)) \/
      M1 = id /\ M2 = L \/ M1 = L /\ M2 = id
  | comp M1 M2, meta_x n as x =>
      (exists a : terms, M1 = shift /\ M2 = cons a x) \/
      M1 = id /\ M2 = x \/ M1 = x /\ M2 = id
  | _, _ => False
  end.
(***********)

Notation invSL := (e_invSL _) (only parsing).
(* <Warning> : Syntax is discontinued *)


Goal forall (b : wsort) (M N : TS b), e_systemSL _ M N -> e_invSL _ M N.
(* Goal: forall (b : wsort) (M N : TS b) (_ : e_systemSL b M N), e_invSL b M N *)
simple induction 1; simple induction 1; intros.
(* app *)
(* Goal: e_invSL wt (env (app a0 b1) s) (app (env a0 s) (env b1 s)) *)
(* Goal: e_invSL wt (env (lambda a0) s) (lambda (env a0 (lift s))) *)
(* Goal: e_invSL wt (env (env a0 s) t) (env a0 (comp s t)) *)
(* Goal: e_invSL wt (env (var n) shift) (var (S n)) *)
(* Goal: e_invSL wt (env (var n) (comp shift s)) (env (var (S n)) s) *)
(* Goal: e_invSL wt (env (var O) (cons a0 s)) a0 *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; left; exists a0; exists b1; auto.
(* lambda *)
(* Goal: e_invSL wt (env (lambda a0) s) (lambda (env a0 (lift s))) *)
(* Goal: e_invSL wt (env (env a0 s) t) (env a0 (comp s t)) *)
(* Goal: e_invSL wt (env (var n) shift) (var (S n)) *)
(* Goal: e_invSL wt (env (var n) (comp shift s)) (env (var (S n)) s) *)
(* Goal: e_invSL wt (env (var O) (cons a0 s)) a0 *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; left; exists a0; auto.
(* clos *)
(* Goal: e_invSL wt (env (env a0 s) t) (env a0 (comp s t)) *)
(* Goal: e_invSL wt (env (var n) shift) (var (S n)) *)
(* Goal: e_invSL wt (env (var n) (comp shift s)) (env (var (S n)) s) *)
(* Goal: e_invSL wt (env (var O) (cons a0 s)) a0 *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; left; exists s; auto.
(* varshift1 *)
(* Goal: e_invSL wt (env (var n) shift) (var (S n)) *)
(* Goal: e_invSL wt (env (var n) (comp shift s)) (env (var (S n)) s) *)
(* Goal: e_invSL wt (env (var O) (cons a0 s)) a0 *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; left; exists n; auto.
(* varshift2 *)
(* Goal: e_invSL wt (env (var n) (comp shift s)) (env (var (S n)) s) *)
(* Goal: e_invSL wt (env (var O) (cons a0 s)) a0 *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; right; left; exists n; auto.
(* fvarcons *)
(* Goal: e_invSL wt (env a0 id) a0 *)
pattern a0 in |- *; apply terms_ind; intros; simpl in |- *.
 (* var *)
(* Goal: or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (env a1 s1)) (@eq (TS ws) s0 (comp s1 (cons (env a1 s0) s))))) (or (@ex nat (fun n : nat => and (@eq (TS wt) (var O) (var n)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp shift s0)) (@eq (TS wt) a1 (var (S n)))))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (env a1 s0) s) (cons (env a1 s0) s1)))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) s0)) (@eq (TS wt) a1 (var O))))) (or (@ex nat (fun n : nat => @ex terms (fun a : terms => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (cons a s0)) (@eq (TS wt) a1 (var n)))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (lift s1)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 shift))))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => @ex sub_explicits (fun t : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) t)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 (comp shift t))))))))) (or (and (@eq (TS wt) (var O) (env a1 s0)) (@eq (TS ws) (cons (env a1 s0) s) id)) (or (and (e_relSL wt (var O) a1) (@eq (TS ws) (cons (env a1 s0) s) s0)) (and (@eq (TS wt) (var O) a1) (e_relSL ws (cons (env a1 s0) s) s0)))))))))) *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 2 right; left; exists s; auto.
 (* app *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS wt) (var O) (lambda a)) (@eq (TS wt) a1 (env a (lift (cons (lambda a1) s)))))) (or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (lambda a1) s) (cons (lambda a1) s0)))) (and (@eq (TS wt) (var O) (lambda a1)) (@eq (TS ws) (cons (lambda a1) s) id))) *)
(* Goal: or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (env a1 s1)) (@eq (TS ws) s0 (comp s1 (cons (env a1 s0) s))))) (or (@ex nat (fun n : nat => and (@eq (TS wt) (var O) (var n)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp shift s0)) (@eq (TS wt) a1 (var (S n)))))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (env a1 s0) s) (cons (env a1 s0) s1)))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) s0)) (@eq (TS wt) a1 (var O))))) (or (@ex nat (fun n : nat => @ex terms (fun a : terms => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (cons a s0)) (@eq (TS wt) a1 (var n)))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (lift s1)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 shift))))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => @ex sub_explicits (fun t : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) t)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 (comp shift t))))))))) (or (and (@eq (TS wt) (var O) (env a1 s0)) (@eq (TS ws) (cons (env a1 s0) s) id)) (or (and (e_relSL wt (var O) a1) (@eq (TS ws) (cons (env a1 s0) s) s0)) (and (@eq (TS wt) (var O) a1) (e_relSL ws (cons (env a1 s0) s) s0)))))))))) *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
right; left; exists s; auto.
 (* lam *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS wt) (var O) (lambda a)) (@eq (TS wt) a1 (env a (lift (cons (lambda a1) s)))))) (or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (lambda a1) s) (cons (lambda a1) s0)))) (and (@eq (TS wt) (var O) (lambda a1)) (@eq (TS ws) (cons (lambda a1) s) id))) *)
(* Goal: or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (env a1 s1)) (@eq (TS ws) s0 (comp s1 (cons (env a1 s0) s))))) (or (@ex nat (fun n : nat => and (@eq (TS wt) (var O) (var n)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp shift s0)) (@eq (TS wt) a1 (var (S n)))))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (env a1 s0) s) (cons (env a1 s0) s1)))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) s0)) (@eq (TS wt) a1 (var O))))) (or (@ex nat (fun n : nat => @ex terms (fun a : terms => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (cons a s0)) (@eq (TS wt) a1 (var n)))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (lift s1)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 shift))))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => @ex sub_explicits (fun t : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) t)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 (comp shift t))))))))) (or (and (@eq (TS wt) (var O) (env a1 s0)) (@eq (TS ws) (cons (env a1 s0) s) id)) (or (and (e_relSL wt (var O) a1) (@eq (TS ws) (cons (env a1 s0) s) s0)) (and (@eq (TS wt) (var O) a1) (e_relSL ws (cons (env a1 s0) s) s0)))))))))) *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
right; left; exists s; auto.
 (* env *)
(* Goal: or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (env a1 s1)) (@eq (TS ws) s0 (comp s1 (cons (env a1 s0) s))))) (or (@ex nat (fun n : nat => and (@eq (TS wt) (var O) (var n)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp shift s0)) (@eq (TS wt) a1 (var (S n)))))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (env a1 s0) s) (cons (env a1 s0) s1)))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) s0)) (@eq (TS wt) a1 (var O))))) (or (@ex nat (fun n : nat => @ex terms (fun a : terms => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (cons a s0)) (@eq (TS wt) a1 (var n)))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (lift s1)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 shift))))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => @ex sub_explicits (fun t : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) t)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 (comp shift t))))))))) (or (and (@eq (TS wt) (var O) (env a1 s0)) (@eq (TS ws) (cons (env a1 s0) s) id)) (or (and (e_relSL wt (var O) a1) (@eq (TS ws) (cons (env a1 s0) s) s0)) (and (@eq (TS wt) (var O) a1) (e_relSL ws (cons (env a1 s0) s) s0)))))))))) *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 2 right; left; exists s; auto.
 (* X *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
left; exists s; auto.
(* fvarlift1 *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS wt) (var O) (lambda a)) (@eq (TS wt) a1 (env a (lift (cons (lambda a1) s)))))) (or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (lambda a1) s) (cons (lambda a1) s0)))) (and (@eq (TS wt) (var O) (lambda a1)) (@eq (TS ws) (cons (lambda a1) s) id))) *)
(* Goal: or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (env a1 s1)) (@eq (TS ws) s0 (comp s1 (cons (env a1 s0) s))))) (or (@ex nat (fun n : nat => and (@eq (TS wt) (var O) (var n)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp shift s0)) (@eq (TS wt) a1 (var (S n)))))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (env a1 s0) s) (cons (env a1 s0) s1)))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) s0)) (@eq (TS wt) a1 (var O))))) (or (@ex nat (fun n : nat => @ex terms (fun a : terms => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (cons a s0)) (@eq (TS wt) a1 (var n)))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (lift s1)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 shift))))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => @ex sub_explicits (fun t : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) t)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 (comp shift t))))))))) (or (and (@eq (TS wt) (var O) (env a1 s0)) (@eq (TS ws) (cons (env a1 s0) s) id)) (or (and (e_relSL wt (var O) a1) (@eq (TS ws) (cons (env a1 s0) s) s0)) (and (@eq (TS wt) (var O) a1) (e_relSL ws (cons (env a1 s0) s) s0)))))))))) *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; right; left; exists s; auto.
(* fvarlift2 *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS wt) (var O) (lambda a)) (@eq (TS wt) a1 (env a (lift (cons (lambda a1) s)))))) (or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (lambda a1) s) (cons (lambda a1) s0)))) (and (@eq (TS wt) (var O) (lambda a1)) (@eq (TS ws) (cons (lambda a1) s) id))) *)
(* Goal: or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (env a1 s1)) (@eq (TS ws) s0 (comp s1 (cons (env a1 s0) s))))) (or (@ex nat (fun n : nat => and (@eq (TS wt) (var O) (var n)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp shift s0)) (@eq (TS wt) a1 (var (S n)))))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (env a1 s0) s) (cons (env a1 s0) s1)))) (or (@ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) s0)) (@eq (TS wt) a1 (var O))))) (or (@ex nat (fun n : nat => @ex terms (fun a : terms => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (cons a s0)) (@eq (TS wt) a1 (var n)))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (lift s1)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 shift))))))) (or (@ex nat (fun n : nat => @ex sub_explicits (fun s1 : sub_explicits => @ex sub_explicits (fun t : sub_explicits => and (@eq (TS wt) (var O) (var (S n))) (and (@eq (TS ws) (cons (env a1 s0) s) (comp (lift s1) t)) (and (@eq (TS wt) a1 (var n)) (@eq (TS ws) s0 (comp s1 (comp shift t))))))))) (or (and (@eq (TS wt) (var O) (env a1 s0)) (@eq (TS ws) (cons (env a1 s0) s) id)) (or (and (e_relSL wt (var O) a1) (@eq (TS ws) (cons (env a1 s0) s) s0)) (and (@eq (TS wt) (var O) a1) (e_relSL ws (cons (env a1 s0) s) s0)))))))))) *)
(* Goal: or (@ex sub_explicits (fun s0 : sub_explicits => and (@eq (TS wt) (var O) (var O)) (@eq (TS ws) (cons (meta_X n) s) (cons (meta_X n) s0)))) (and (@eq (TS wt) (var O) (meta_X n)) (@eq (TS ws) (cons (meta_X n) s) id)) *)
(* Goal: e_invSL wt (env (var O) (lift s)) (var O) *)
(* Goal: e_invSL wt (env (var O) (comp (lift s) t)) (env (var O) t) *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 3 right; left; exists s; auto.
(* rvarcons *)
(* Goal: e_invSL wt (env (var (S n)) (cons a0 s)) (env (var n) s) *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 4 right; left; exists n; exists a0; auto.
(* rvarlift1 *)
(* Goal: e_invSL wt (env (var (S n)) (lift s)) (env (var n) (comp s shift)) *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 5 right; left; exists n; exists s; auto.
(* rvarlift2 *)
(* Goal: e_invSL wt (env (var (S n)) (comp (lift s) t)) (env (var n) (comp s (comp shift t))) *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 6 right; left; exists n; exists s; exists t; auto.
(* assenv *)
(* Goal: e_invSL ws (comp (comp s0 t0) u) (comp s0 (comp t0 u)) *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; left; exists t0; auto.
(* mapenv *)
(* Goal: e_invSL ws (comp (cons a s0) t0) (cons (env a t0) (comp s0 t0)) *)
(* Goal: e_invSL ws (comp shift (cons a s0)) s0 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; left; exists a; exists s0; auto.
(* shiftcons *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
pattern s0 in |- *; apply sub_explicits_ind; intros; simpl in |- *.
 (* id *)
(* Goal: or (@ex terms (fun a0 : terms => and (@eq (TS ws) shift shift) (@eq (TS ws) (cons a (meta_x n)) (cons a0 (meta_x n))))) (or (and (@eq (TS ws) shift id) (@eq (TS ws) (cons a (meta_x n)) (meta_x n))) (and (@eq (TS ws) shift (meta_x n)) (@eq (TS ws) (cons a (meta_x n)) id))) *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
left; exists a; auto.
 (*| *)
(* Goal: or (@ex terms (fun a0 : terms => and (@eq (TS ws) shift shift) (@eq (TS ws) (cons a (meta_x n)) (cons a0 (meta_x n))))) (or (and (@eq (TS ws) shift id) (@eq (TS ws) (cons a (meta_x n)) (meta_x n))) (and (@eq (TS ws) shift (meta_x n)) (@eq (TS ws) (cons a (meta_x n)) id))) *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
left; exists a; auto.
 (* . *)
(* Goal: or (@ex terms (fun a0 : terms => and (@eq (TS ws) shift shift) (@eq (TS ws) (cons a (meta_x n)) (cons a0 (meta_x n))))) (or (and (@eq (TS ws) shift id) (@eq (TS ws) (cons a (meta_x n)) (meta_x n))) (and (@eq (TS ws) shift (meta_x n)) (@eq (TS ws) (cons a (meta_x n)) id))) *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
right; left; exists a; auto.
 (* o *)
(* Goal: or (@ex terms (fun a0 : terms => and (@eq (TS ws) shift shift) (@eq (TS ws) (cons a (meta_x n)) (cons a0 (meta_x n))))) (or (and (@eq (TS ws) shift id) (@eq (TS ws) (cons a (meta_x n)) (meta_x n))) (and (@eq (TS ws) shift (meta_x n)) (@eq (TS ws) (cons a (meta_x n)) id))) *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
right; left; exists a; auto.
 (*|| *)
(* Goal: or (@ex terms (fun a0 : terms => and (@eq (TS ws) shift shift) (@eq (TS ws) (cons a (meta_x n)) (cons a0 (meta_x n))))) (or (and (@eq (TS ws) shift id) (@eq (TS ws) (cons a (meta_x n)) (meta_x n))) (and (@eq (TS ws) shift (meta_x n)) (@eq (TS ws) (cons a (meta_x n)) id))) *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
left; exists a; auto.
 (* x *)
(* Goal: or (@ex terms (fun a0 : terms => and (@eq (TS ws) shift shift) (@eq (TS ws) (cons a (meta_x n)) (cons a0 (meta_x n))))) (or (and (@eq (TS ws) shift id) (@eq (TS ws) (cons a (meta_x n)) (meta_x n))) (and (@eq (TS ws) shift (meta_x n)) (@eq (TS ws) (cons a (meta_x n)) id))) *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
left; exists a; auto.
(* shiftlift1 *)
(* Goal: e_invSL ws (comp shift (lift s0)) (comp s0 shift) *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 2 right; left; auto.
(* shiftlift2 *)
(* Goal: e_invSL ws (comp shift (comp (lift s0) t0)) (comp s0 (comp shift t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 3 right; left; exists t0; auto.
(* lift1 *)
(* Goal: e_invSL ws (comp (lift s0) (lift t0)) (lift (comp s0 t0)) *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; right; left; exists s0; exists t0; auto.
(* lift2 *)
(* Goal: e_invSL ws (comp (lift s0) (comp (lift t0) u)) (comp (lift (comp s0 t0)) u) *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; do 4 right; left; exists s0; exists t0; auto.
(* liftenv *)
(* Goal: e_invSL ws (comp (lift s0) (cons a t0)) (cons a (comp s0 t0)) *)
(* Goal: e_invSL ws (comp id s0) s0 *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; right; right; left; exists s0; exists t0; auto.
(* idl *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
pattern s0 in |- *; apply sub_explicits_ind; intros; simpl in |- *.
 (* id *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
right; auto.
 (*| *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
right; left; auto.
 (* . *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 3 right; left; auto.
 (* o *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 5 right; left; auto.
 (*|| *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 2 right; left; auto.
 (* x *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
right; left; auto.
(* idr *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
pattern s0 in |- *; apply sub_explicits_ind; intros; simpl in |- *.
 (* id *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
right; auto.
 (*| *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
right; right; auto.
 (* . *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
do 4 right; auto.
 (* o *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 6 right; left; auto.
 (*|| *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
do 3 right; auto.
 (* x *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
right; right; auto.
(* liftid *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
simpl in |- *; auto.
(* id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
pattern a0 in |- *; apply terms_ind; intros; simpl in |- *.
 (* var *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
do 3 right; auto.
 (* app *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
do 2 right; auto.
 (* lam *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
do 2 right; auto.
 (* env *)
(* Goal: or (@ex terms (fun a : terms => and (@eq (TS ws) id shift) (@eq (TS ws) (meta_x n) (cons a (meta_x n))))) (or (and (@eq (TS ws) id id) (@eq (TS ws) (meta_x n) (meta_x n))) (and (@eq (TS ws) id (meta_x n)) (@eq (TS ws) (meta_x n) id))) *)
(* Goal: e_invSL ws (comp s0 id) s0 *)
(* Goal: e_invSL ws (lift id) id *)
(* Goal: e_invSL wt (env a0 id) a0 *)
do 7 right; left; auto.
 (* X *)
(* Goal: or (@ex sub_explicits (fun s : sub_explicits => and (@eq (TS wt) (meta_X n) (var O)) (@eq (TS ws) id (cons (meta_X n) s)))) (and (@eq (TS wt) (meta_X n) (meta_X n)) (@eq (TS ws) id id)) *)
right; auto.
Save lemma1_inv_systemSL.
Hint Resolve lemma1_inv_systemSL.

Goal forall (b : wsort) (M N : TS b), e_relSL _ M N -> e_invSL _ M N.
(* Goal: forall (b : wsort) (M N : TS b) (_ : e_relSL b M N), e_invSL b M N *)
simple induction 1; intros; simpl in |- *; auto 11.
Save lemma1_invSL.
Hint Resolve lemma1_invSL.










