Library env








Typing Environment for annotated terms .



  As for Terms, we define contexts of "Annotated" terms, with the very 
  safe function and tools as for the usual one.





Require Import base term.



Require Import List.



Require Import Peano_dec.



Require Import Compare_dec.



Require Import Lt Le Gt.






Module Type env_mod (X:term_sig) (TM:term_mod X).
Interactive Module Type env_mod started





Import TM.










Very naive definition of environment : list of term 


 


 be carefull, the usual written env Γ(x:A) is encoded in 
  A::Γ









Definition Env := list Term.
Env is defined








Set Implicit Arguments.



Inductive item (A:Type) (x:A): list A ->nat->Prop :=

  | item_hd: forall l:list A, (item x (cons x l) O)

  | item_tl: forall (l:list A)(n:nat)(y:A), item x l n -> item x (cons y l) (S n).
item is defined
item_ind is defined








Hint Constructors item.






Notation " x ↓ n ∈ Γ " := (item x Γ n) (at level 80, no associativity) : Typ_scope.






Lemma fun_item: forall A (u v:A)(Γ:list A)(n:nat), 

  u ↓ n ∈ Γ -> v ↓ n ∈ Γ -> u=v.
1 subgoals, subgoal 1 (ID 7)
  
  ============================
   forall (A : Type) (u v : A) (Γ : list A) (n : nat),
   u ↓ n ∈ Γ -> v ↓ n ∈ Γ -> u = v

(dependent evars:)





intros A u v e n;

generalize A u v e; clear A u v e.
1 subgoals, subgoal 1 (ID 14)
  
  n : nat
  ============================
   forall (A : Type) (u v : A) (e : list A), u ↓ n ∈ e -> v ↓ n ∈ e -> u = v

(dependent evars:)





induction n; intros.
2 subgoals, subgoal 1 (ID 26)
  
  A : Type
  u : A
  v : A
  e : list A
  H : u ↓ 0 ∈ e
  H0 : v ↓ 0 ∈ e
  ============================
   u = v

subgoal 2 (ID 32) is:
 u = v
(dependent evars:)





inversion H; inversion H0.
2 subgoals, subgoal 1 (ID 77)
  
  A : Type
  u : A
  v : A
  e : list A
  H : u ↓ 0 ∈ e
  H0 : v ↓ 0 ∈ e
  l : list A
  H1 : u :: l = e
  l0 : list A
  H2 : v :: l0 = e
  ============================
   u = v

subgoal 2 (ID 32) is:
 u = v
(dependent evars:)





rewrite <- H2 in H1; injection H1; trivial.
1 subgoals, subgoal 1 (ID 32)
  
  n : nat
  IHn : forall (A : Type) (u v : A) (e : list A),
        u ↓ n ∈ e -> v ↓ n ∈ e -> u = v
  A : Type
  u : A
  v : A
  e : list A
  H : u ↓ S n ∈ e
  H0 : v ↓ S n ∈ e
  ============================
   u = v

(dependent evars:)





inversion H; inversion H0; subst.
1 subgoals, subgoal 1 (ID 207)
  
  n : nat
  IHn : forall (A : Type) (u v : A) (e : list A),
        u ↓ n ∈ e -> v ↓ n ∈ e -> u = v
  A : Type
  u : A
  v : A
  l : list A
  y : A
  H3 : u ↓ n ∈ l
  l0 : list A
  y0 : A
  H6 : v ↓ n ∈ l0
  H : u ↓ S n ∈ y :: l
  H0 : v ↓ S n ∈ y :: l
  H5 : y0 :: l0 = y :: l
  ============================
   u = v

(dependent evars:)





injection H5; intros; subst.
1 subgoals, subgoal 1 (ID 228)
  
  n : nat
  IHn : forall (A : Type) (u v : A) (e : list A),
        u ↓ n ∈ e -> v ↓ n ∈ e -> u = v
  A : Type
  u : A
  v : A
  l : list A
  y : A
  H3 : u ↓ n ∈ l
  H : u ↓ S n ∈ y :: l
  H0 : v ↓ S n ∈ y :: l
  H6 : v ↓ n ∈ l
  H5 : y :: l = y :: l
  ============================
   u = v

(dependent evars:)





apply IHn with (e:=l); trivial.
No more subgoals.
(dependent evars:)





Qed.
fun_item is defined








Inductive trunc (A:Type) : nat->list A ->list A->Prop :=

     trunc_O: forall (Γ:list A) , (trunc O Γ Γ)

   | trunc_S: forall (k:nat)(Γ Γ':list A)(x:A), trunc k Γ Γ' 

                -> trunc (S k) (cons x Γ) Γ'.
trunc is defined
trunc_ind is defined








Hint Constructors trunc.






Lemma item_trunc: forall (A:Type) (n:nat) (Γ:list A) (t:A), 

  t ↓ n ∈ Γ -> exists f , trunc (S n) Γ f.
1 subgoals, subgoal 1 (ID 236)
  
  ============================
   forall (A : Type) (n : nat) (Γ : list A) (t : A),
   t ↓ n ∈ Γ -> exists f : list A, trunc (S n) Γ f

(dependent evars:)





intros A n; induction n; intros.
2 subgoals, subgoal 1 (ID 247)
  
  A : Type
  Γ : list A
  t : A
  H : t ↓ 0 ∈ Γ
  ============================
   exists f : list A, trunc 1 Γ f

subgoal 2 (ID 250) is:
 exists f : list A, trunc (S (S n)) Γ f
(dependent evars:)





inversion H.
2 subgoals, subgoal 1 (ID 265)
  
  A : Type
  Γ : list A
  t : A
  H : t ↓ 0 ∈ Γ
  l : list A
  H0 : t :: l = Γ
  ============================
   exists f : list A, trunc 1 (t :: l) f

subgoal 2 (ID 250) is:
 exists f : list A, trunc (S (S n)) Γ f
(dependent evars:)





exists l.
2 subgoals, subgoal 1 (ID 291)
  
  A : Type
  Γ : list A
  t : A
  H : t ↓ 0 ∈ Γ
  l : list A
  H0 : t :: l = Γ
  ============================
   trunc 1 (t :: l) l

subgoal 2 (ID 250) is:
 exists f : list A, trunc (S (S n)) Γ f
(dependent evars:)





apply trunc_S; apply trunc_O.
1 subgoals, subgoal 1 (ID 250)
  
  A : Type
  n : nat
  IHn : forall (Γ : list A) (t : A),
        t ↓ n ∈ Γ -> exists f : list A, trunc (S n) Γ f
  Γ : list A
  t : A
  H : t ↓ S n ∈ Γ
  ============================
   exists f : list A, trunc (S (S n)) Γ f

(dependent evars:)





inversion H; subst.
1 subgoals, subgoal 1 (ID 348)
  
  A : Type
  n : nat
  IHn : forall (Γ : list A) (t : A),
        t ↓ n ∈ Γ -> exists f : list A, trunc (S n) Γ f
  t : A
  l : list A
  y : A
  H2 : t ↓ n ∈ l
  H : t ↓ S n ∈ y :: l
  ============================
   exists f : list A, trunc (S (S n)) (y :: l) f

(dependent evars:)





destruct (IHn l t H2).
1 subgoals, subgoal 1 (ID 355)
  
  A : Type
  n : nat
  IHn : forall (Γ : list A) (t : A),
        t ↓ n ∈ Γ -> exists f : list A, trunc (S n) Γ f
  t : A
  l : list A
  y : A
  H2 : t ↓ n ∈ l
  H : t ↓ S n ∈ y :: l
  x : list A
  H0 : trunc (S n) l x
  ============================
   exists f : list A, trunc (S (S n)) (y :: l) f

(dependent evars:)





exists x.
1 subgoals, subgoal 1 (ID 357)
  
  A : Type
  n : nat
  IHn : forall (Γ : list A) (t : A),
        t ↓ n ∈ Γ -> exists f : list A, trunc (S n) Γ f
  t : A
  l : list A
  y : A
  H2 : t ↓ n ∈ l
  H : t ↓ S n ∈ y :: l
  x : list A
  H0 : trunc (S n) l x
  ============================
   trunc (S (S n)) (y :: l) x

(dependent evars:)





apply trunc_S.
1 subgoals, subgoal 1 (ID 358)
  
  A : Type
  n : nat
  IHn : forall (Γ : list A) (t : A),
        t ↓ n ∈ Γ -> exists f : list A, trunc (S n) Γ f
  t : A
  l : list A
  y : A
  H2 : t ↓ n ∈ l
  H : t ↓ S n ∈ y :: l
  x : list A
  H0 : trunc (S n) l x
  ============================
   trunc (S n) l x

(dependent evars:)





apply H0.
No more subgoals.
(dependent evars:)





Qed.
item_trunc is defined















insert a type d1 in an env Γ : BE CAREFULL d1 is not checked to be a valid type in Γ 
  it takes care of the DeBruijn lift when need 





Inductive ins_in_env (Γ:Env ) (d1:Term): nat->Env -> Env  ->Prop :=

  | ins_O: ins_in_env Γ d1 O Γ (d1::Γ)

  | ins_S: forall (n:nat)(Δ Δ':Env )(d:Term), (ins_in_env Γ d1 n Δ Δ')

    -> ins_in_env Γ d1 (S n) (d::Δ) ( (d ↑ 1 # n)::Δ' ).
ins_in_env is defined
ins_in_env_ind is defined








Hint Constructors ins_in_env.






Lemma ins_item_ge: forall (d':Term) (n:nat) (Γ Δ Δ':Env), 

  ins_in_env Γ d' n Δ Δ' -> 

  forall (v:nat), n<=v -> 

 forall (d:Term),  d ↓ v ∈ Δ  -> d ↓ (S v) ∈ Δ'.
1 subgoals, subgoal 1 (ID 364)
  
  ============================
   forall (d' : Term) (n : nat) (Γ Δ Δ' : Env),
   ins_in_env Γ d' n Δ Δ' ->
   forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'

(dependent evars:)





induction n; intros.
2 subgoals, subgoal 1 (ID 380)
  
  d' : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' 0 Δ Δ'
  v : nat
  H0 : 0 <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↓ S v ∈ Δ'

subgoal 2 (ID 388) is:
 d ↓ S v ∈ Δ'
(dependent evars:)





inversion H; subst.
2 subgoals, subgoal 1 (ID 442)
  
  d' : Term
  Δ : Env
  v : nat
  H0 : 0 <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  H : ins_in_env Δ d' 0 Δ (d' :: Δ)
  ============================
   d ↓ S v ∈ d' :: Δ

subgoal 2 (ID 388) is:
 d ↓ S v ∈ Δ'
(dependent evars:)





apply item_tl. 
2 subgoals, subgoal 1 (ID 443)
  
  d' : Term
  Δ : Env
  v : nat
  H0 : 0 <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  H : ins_in_env Δ d' 0 Δ (d' :: Δ)
  ============================
   d ↓ v ∈ Δ

subgoal 2 (ID 388) is:
 d ↓ S v ∈ Δ'
(dependent evars:)



exact H1.
1 subgoals, subgoal 1 (ID 388)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' (S n) Δ Δ'
  v : nat
  H0 : S n <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↓ S v ∈ Δ'

(dependent evars:)





inversion H; subst.
1 subgoals, subgoal 1 (ID 506)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↓ S v ∈ d0 ↑ 1 # n :: Δ'0

(dependent evars:)





apply item_tl.
1 subgoals, subgoal 1 (ID 507)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↓ v ∈ Δ'0

(dependent evars:)





destruct v.
2 subgoals, subgoal 1 (ID 517)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  H0 : S n <= 0
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ 0 ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↓ 0 ∈ Δ'0

subgoal 2 (ID 523) is:
 d ↓ S v ∈ Δ'0
(dependent evars:)





elim (le_Sn_O n H0).
1 subgoals, subgoal 1 (ID 523)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↓ S v ∈ Δ'0

(dependent evars:)





apply IHn with (Γ:=Γ) (Δ:=Δ0).
3 subgoals, subgoal 1 (ID 524)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   ins_in_env Γ d' n Δ0 Δ'0

subgoal 2 (ID 525) is:
 n <= v
subgoal 3 (ID 526) is:
 d ↓ v ∈ Δ0
(dependent evars:)





trivial.
2 subgoals, subgoal 1 (ID 525)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   n <= v

subgoal 2 (ID 526) is:
 d ↓ v ∈ Δ0
(dependent evars:)





apply le_S_n ; trivial.
1 subgoals, subgoal 1 (ID 526)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)





inversion H1.
1 subgoals, subgoal 1 (ID 597)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  l : list Term
  n0 : nat
  y : Term
  H4 : d ↓ v ∈ Δ0
  H2 : y = d0
  H5 : l = Δ0
  H6 : n0 = v
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)





exact H4.
No more subgoals.
(dependent evars:)





Qed.
ins_item_ge is defined








Lemma gt_O: forall v, ~ 0 > v.
1 subgoals, subgoal 1 (ID 603)
  
  ============================
   forall v : nat, ~ 0 > v

(dependent evars:)





intros; intro.
1 subgoals, subgoal 1 (ID 606)
  
  v : nat
  H : 0 > v
  ============================
   False

(dependent evars:)





unfold gt in H. 
1 subgoals, subgoal 1 (ID 607)
  
  v : nat
  H : v < 0
  ============================
   False

(dependent evars:)



apply lt_n_O in H; trivial.
No more subgoals.
(dependent evars:)





Qed.
gt_O is defined








Lemma ins_item_lt: forall (d':Term)(n:nat)(Γ Δ Δ':Env),

 ins_in_env Γ d' n Δ Δ' ->

 forall (v:nat), n > v ->

 forall (d:Term), d ↓ v ∈ Δ -> (d ↑ 1 # (n-S v)) ↓ v ∈ Δ' .
1 subgoals, subgoal 1 (ID 612)
  
  ============================
   forall (d' : Term) (n : nat) (Γ Δ Δ' : Env),
   ins_in_env Γ d' n Δ Δ' ->
   forall v : nat,
   n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'

(dependent evars:)





induction n; intros.
2 subgoals, subgoal 1 (ID 628)
  
  d' : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' 0 Δ Δ'
  v : nat
  H0 : 0 > v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↑ 1 # (0 - S v) ↓ v ∈ Δ'

subgoal 2 (ID 636) is:
 d ↑ 1 # (S n - S v) ↓ v ∈ Δ'
(dependent evars:)





elim (gt_O H0).
1 subgoals, subgoal 1 (ID 636)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' (S n) Δ Δ'
  v : nat
  H0 : S n > v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↑ 1 # (S n - S v) ↓ v ∈ Δ'

(dependent evars:)





inversion H; subst.
1 subgoals, subgoal 1 (ID 700)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↑ 1 # (S n - S v) ↓ v ∈ d0 ↑ 1 # n :: Δ'0

(dependent evars:)





destruct v.
2 subgoals, subgoal 1 (ID 710)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  H0 : S n > 0
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ 0 ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↑ 1 # (S n - 1) ↓ 0 ∈ d0 ↑ 1 # n :: Δ'0

subgoal 2 (ID 716) is:
 d ↑ 1 # (S n - S (S v)) ↓ S v ∈ d0 ↑ 1 # n :: Δ'0
(dependent evars:)





inversion H1; subst.
2 subgoals, subgoal 1 (ID 785)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  H0 : S n > 0
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  H1 : d0 ↓ 0 ∈ d0 :: Δ0
  ============================
   d0 ↑ 1 # (S n - 1) ↓ 0 ∈ d0 ↑ 1 # n :: Δ'0

subgoal 2 (ID 716) is:
 d ↑ 1 # (S n - S (S v)) ↓ S v ∈ d0 ↑ 1 # n :: Δ'0
(dependent evars:)





replace (S n -1) with n by intuition.
2 subgoals, subgoal 1 (ID 789)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  H0 : S n > 0
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  H1 : d0 ↓ 0 ∈ d0 :: Δ0
  ============================
   d0 ↑ 1 # n ↓ 0 ∈ d0 ↑ 1 # n :: Δ'0

subgoal 2 (ID 716) is:
 d ↑ 1 # (S n - S (S v)) ↓ S v ∈ d0 ↑ 1 # n :: Δ'0
(dependent evars:)





apply item_hd.
1 subgoals, subgoal 1 (ID 716)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↑ 1 # (S n - S (S v)) ↓ S v ∈ d0 ↑ 1 # n :: Δ'0

(dependent evars:)





apply item_tl.
1 subgoals, subgoal 1 (ID 805)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↑ 1 # (S n - S (S v)) ↓ v ∈ Δ'0

(dependent evars:)





replace (S n - S (S v)) with (n -S v) by intuition.
1 subgoals, subgoal 1 (ID 809)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↑ 1 # (n - S v) ↓ v ∈ Δ'0

(dependent evars:)





apply IHn with (Γ:=Γ) (Δ:=Δ0).
3 subgoals, subgoal 1 (ID 812)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   ins_in_env Γ d' n Δ0 Δ'0

subgoal 2 (ID 813) is:
 n > v
subgoal 3 (ID 814) is:
 d ↓ v ∈ Δ0
(dependent evars:)





exact H3.
2 subgoals, subgoal 1 (ID 813)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   n > v

subgoal 2 (ID 814) is:
 d ↓ v ∈ Δ0
(dependent evars:)





intuition.
1 subgoals, subgoal 1 (ID 814)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)





inversion H1.
1 subgoals, subgoal 1 (ID 900)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑ 1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑ 1 # n :: Δ'0)
  l : list Term
  n0 : nat
  y : Term
  H4 : d ↓ v ∈ Δ0
  H2 : y = d0
  H5 : l = Δ0
  H6 : n0 = v
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)





exact H4.
No more subgoals.
(dependent evars:)





Qed.
ins_item_lt is defined








Definition item_lift (t:Term) (Γ:Env) (n:nat) :=

     exists u ,  t= u ↑ (S n) /\  u ↓ n ∈ Γ .
item_lift is defined








Hint Unfold item_lift.



Notation " t ↓ n ⊂ Γ " := (item_lift t Γ n) (at level 80, no associativity): Typ_scope.






Lemma ins_item_lift_lt: forall  (d':Term)(n:nat)(Γ Δ Δ':Env ),

 ins_in_env Γ d' n Δ Δ' ->

 forall (v:nat),  n>v ->

 forall (t:Term), t ↓ v ⊂ Δ  -> (t ↑ 1 # n) ↓ v ⊂ Δ'.
1 subgoals, subgoal 1 (ID 908)
  
  ============================
   forall (d' : Term) (n : nat) (Γ Δ Δ' : Env),
   ins_in_env Γ d' n Δ Δ' ->
   forall v : nat, n > v -> forall t : Term, t ↓ v ⊂ Δ -> t ↑ 1 # n ↓ v ⊂ Δ'

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 918)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  H1 : t ↓ v ⊂ Δ
  ============================
   t ↑ 1 # n ↓ v ⊂ Δ'

(dependent evars:)





destruct H1 as [u [ P Q]].
1 subgoals, subgoal 1 (ID 926)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   t ↑ 1 # n ↓ v ⊂ Δ'

(dependent evars:)





rewrite P.
1 subgoals, subgoal 1 (ID 927)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ (S v) ↑ 1 # n ↓ v ⊂ Δ'

(dependent evars:)





exists (u ↑ 1 # (n - S v) ); split.
2 subgoals, subgoal 1 (ID 931)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ (S v) ↑ 1 # n = u ↑ 1 # (n - S v) ↑ (S v)

subgoal 2 (ID 932) is:
 u ↑ 1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)





replace n with ( S v + (n -  S v))  by intuition.
2 subgoals, subgoal 1 (ID 936)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ (S v) ↑ 1 # (S v + (n - S v)) =
   u ↑ 1 # (S v + (n - S v) - S v) ↑ (S v)

subgoal 2 (ID 932) is:
 u ↑ 1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)





rewrite liftP2.
3 subgoals, subgoal 1 (ID 953)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ 1 # (n - S v) ↑ (S v) = u ↑ 1 # (S v + (n - S v) - S v) ↑ (S v)

subgoal 2 (ID 954) is:
 0 <= n - S v
subgoal 3 (ID 932) is:
 u ↑ 1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)





replace (S v+(n-S v)-S v) with (n-S v) by intuition.
3 subgoals, subgoal 1 (ID 958)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ 1 # (n - S v) ↑ (S v) = u ↑ 1 # (n - S v) ↑ (S v)

subgoal 2 (ID 954) is:
 0 <= n - S v
subgoal 3 (ID 932) is:
 u ↑ 1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)





reflexivity.
2 subgoals, subgoal 1 (ID 954)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   0 <= n - S v

subgoal 2 (ID 932) is:
 u ↑ 1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)





intuition.
1 subgoals, subgoal 1 (ID 932)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑ (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ 1 # (n - S v) ↓ v ∈ Δ'

(dependent evars:)





clear t P.
1 subgoals, subgoal 1 (ID 989)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  u : Term
  Q : u ↓ v ∈ Δ
  ============================
   u ↑ 1 # (n - S v) ↓ v ∈ Δ'

(dependent evars:)





inversion H; subst.
2 subgoals, subgoal 1 (ID 1056)
  
  d' : Term
  Δ : Env
  v : nat
  u : Term
  Q : u ↓ v ∈ Δ
  H0 : 0 > v
  H : ins_in_env Δ d' 0 Δ (d' :: Δ)
  ============================
   u ↑ 1 # (0 - S v) ↓ v ∈ d' :: Δ

subgoal 2 (ID 1073) is:
 u ↑ 1 # (S n0 - S v) ↓ v ∈ d ↑ 1 # n0 :: Δ'0
(dependent evars:)





elim (gt_O H0).
1 subgoals, subgoal 1 (ID 1073)
  
  d' : Term
  Γ : Env
  v : nat
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  Q : u ↓ v ∈ d :: Δ0
  H0 : S n0 > v
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  ============================
   u ↑ 1 # (S n0 - S v) ↓ v ∈ d ↑ 1 # n0 :: Δ'0

(dependent evars:)





inversion Q; subst.
2 subgoals, subgoal 1 (ID 1151)
  
  d' : Term
  Γ : Env
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  H0 : S n0 > 0
  Q : d ↓ 0 ∈ d :: Δ0
  ============================
   d ↑ 1 # (S n0 - 1) ↓ 0 ∈ d ↑ 1 # n0 :: Δ'0

subgoal 2 (ID 1159) is:
 u ↑ 1 # (S n0 - S (S n)) ↓ S n ∈ d ↑ 1 # n0 :: Δ'0
(dependent evars:)





replace (S n0 -1) with n0 by intuition.
2 subgoals, subgoal 1 (ID 1163)
  
  d' : Term
  Γ : Env
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  H0 : S n0 > 0
  Q : d ↓ 0 ∈ d :: Δ0
  ============================
   d ↑ 1 # n0 ↓ 0 ∈ d ↑ 1 # n0 :: Δ'0

subgoal 2 (ID 1159) is:
 u ↑ 1 # (S n0 - S (S n)) ↓ S n ∈ d ↑ 1 # n0 :: Δ'0
(dependent evars:)





apply item_hd.
1 subgoals, subgoal 1 (ID 1159)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   u ↑ 1 # (S n0 - S (S n)) ↓ S n ∈ d ↑ 1 # n0 :: Δ'0

(dependent evars:)





apply item_tl.
1 subgoals, subgoal 1 (ID 1178)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   u ↑ 1 # (S n0 - S (S n)) ↓ n ∈ Δ'0

(dependent evars:)





replace (S n0 - S (S n)) with (n0 -S n) by intuition.
1 subgoals, subgoal 1 (ID 1182)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   u ↑ 1 # (n0 - S n) ↓ n ∈ Δ'0

(dependent evars:)





apply ins_item_lt with d' Γ Δ0; trivial.
1 subgoals, subgoal 1 (ID 1186)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑ 1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   n0 > n

(dependent evars:)





intuition.
No more subgoals.
(dependent evars:)





Qed.
ins_item_lift_lt is defined















if Γ == Γ1 (x:T) Γ2   and Γ1 ⊢ t:T  and Γ1 as size n 
   then Γn← t = Γ1 (Γ2x ← t)









Inductive sub_in_env (Γ : Env) (t T:Term):

  nat -> Env -> Env -> Prop :=

    | sub_O :  sub_in_env Γ t T 0 (T :: Γ) Γ

    | sub_S :

        forall Δ Δ' n  B,

        sub_in_env Γ t T n Δ Δ' ->

        sub_in_env Γ t T (S n) (B :: Δ) ( B [n← t]  :: Δ').
sub_in_env is defined
sub_in_env_ind is defined








Hint Constructors sub_in_env.






Lemma nth_sub_sup :

   forall n Γ Δ Δ' t T,

   sub_in_env Γ t T n Δ Δ' ->

   forall v : nat, n <= v -> 

   forall d , d ↓ (S v) ∈ Δ -> d ↓ v ∈ Δ'.
1 subgoals, subgoal 1 (ID 1220)
  
  ============================
   forall (n : nat) (Γ Δ Δ' : Env) (t T : Term),
   sub_in_env Γ t T n Δ Δ' ->
   forall v : nat, n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'

(dependent evars:)





intros n Γ Δ Δ' t T H; induction H; intros.
2 subgoals, subgoal 1 (ID 1247)
  
  Γ : Env
  t : Term
  T : Term
  v : nat
  H : 0 <= v
  d : Term
  H0 : d ↓ S v ∈ T :: Γ
  ============================
   d ↓ v ∈ Γ

subgoal 2 (ID 1251) is:
 d ↓ v ∈ B [n ← t] :: Δ'
(dependent evars:)





inversion H0; subst. 
2 subgoals, subgoal 1 (ID 1328)
  
  Γ : Env
  t : Term
  T : Term
  v : nat
  H : 0 <= v
  d : Term
  H0 : d ↓ S v ∈ T :: Γ
  H2 : d ↓ v ∈ Γ
  ============================
   d ↓ v ∈ Γ

subgoal 2 (ID 1251) is:
 d ↓ v ∈ B [n ← t] :: Δ'
(dependent evars:)



trivial.
1 subgoals, subgoal 1 (ID 1251)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  ============================
   d ↓ v ∈ B [n ← t] :: Δ'

(dependent evars:)





inversion H1; subst.
1 subgoals, subgoal 1 (ID 1405)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d ↓ v ∈ B [n ← t] :: Δ'

(dependent evars:)





destruct v.
2 subgoals, subgoal 1 (ID 1415)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  H0 : S n <= 0
  d : Term
  H1 : d ↓ 1 ∈ B :: Δ
  H3 : d ↓ 0 ∈ Δ
  ============================
   d ↓ 0 ∈ B [n ← t] :: Δ'

subgoal 2 (ID 1421) is:
 d ↓ S v ∈ B [n ← t] :: Δ'
(dependent evars:)





elim (le_Sn_O n H0).
1 subgoals, subgoal 1 (ID 1421)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= S v
  d : Term
  H1 : d ↓ S (S v) ∈ B :: Δ
  H3 : d ↓ S v ∈ Δ
  ============================
   d ↓ S v ∈ B [n ← t] :: Δ'

(dependent evars:)





apply item_tl.
1 subgoals, subgoal 1 (ID 1422)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= S v
  d : Term
  H1 : d ↓ S (S v) ∈ B :: Δ
  H3 : d ↓ S v ∈ Δ
  ============================
   d ↓ v ∈ Δ'

(dependent evars:)





apply le_S_n in H0.
1 subgoals, subgoal 1 (ID 1424)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : n <= v
  d : Term
  H1 : d ↓ S (S v) ∈ B :: Δ
  H3 : d ↓ S v ∈ Δ
  ============================
   d ↓ v ∈ Δ'

(dependent evars:)





apply IHsub_in_env; trivial.
No more subgoals.
(dependent evars:)





Qed.
nth_sub_sup is defined








Lemma nth_sub_eq :

   forall t T n Γ Δ Δ',

   sub_in_env Γ t T n Δ Δ' -> 

  forall d , d↓ n ∈ Δ -> T = d.
1 subgoals, subgoal 1 (ID 1436)
  
  ============================
   forall (t T : Term) (n : nat) (Γ Δ Δ' : Env),
   sub_in_env Γ t T n Δ Δ' -> forall d : Term, d ↓ n ∈ Δ -> T = d

(dependent evars:)





intros  t T n Γ Δ Δ' H; induction H; intros.
2 subgoals, subgoal 1 (ID 1461)
  
  t : Term
  T : Term
  Γ : Env
  d : Term
  H : d ↓ 0 ∈ T :: Γ
  ============================
   T = d

subgoal 2 (ID 1463) is:
 T = d
(dependent evars:)





inversion H; trivial.
1 subgoals, subgoal 1 (ID 1463)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall d : Term, d ↓ n ∈ Δ -> T = d
  d : Term
  H0 : d ↓ S n ∈ B :: Δ
  ============================
   T = d

(dependent evars:)





inversion H0; subst.
1 subgoals, subgoal 1 (ID 1603)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall d : Term, d ↓ n ∈ Δ -> T = d
  d : Term
  H0 : d ↓ S n ∈ B :: Δ
  H2 : d ↓ n ∈ Δ
  ============================
   T = d

(dependent evars:)





apply IHsub_in_env; trivial.
No more subgoals.
(dependent evars:)





Qed.
nth_sub_eq is defined








Lemma nth_sub_inf :

   forall t T n Γ Δ Δ',

   sub_in_env Γ t T n Δ Δ' ->

   forall v : nat,

   n > v ->

   forall d , d ↓ v ∈ Δ ->  ( d [n - S v ← t] )↓ v ∈ Δ' .
1 subgoals, subgoal 1 (ID 1614)
  
  ============================
   forall (t T : Term) (n : nat) (Γ Δ Δ' : Env),
   sub_in_env Γ t T n Δ Δ' ->
   forall v : nat,
   n > v -> forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'

(dependent evars:)





intros t T n Γ Δ Δ' H; induction H; intros.
2 subgoals, subgoal 1 (ID 1641)
  
  t : Term
  T : Term
  Γ : Env
  v : nat
  H : 0 > v
  d : Term
  H0 : d ↓ v ∈ T :: Γ
  ============================
   d [(0 - S v) ← t] ↓ v ∈ Γ

subgoal 2 (ID 1645) is:
 d [(S n - S v) ← t] ↓ v ∈ B [n ← t] :: Δ'
(dependent evars:)





elim (gt_O  H).
1 subgoals, subgoal 1 (ID 1645)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > v
  d : Term
  H1 : d ↓ v ∈ B :: Δ
  ============================
   d [(S n - S v) ← t] ↓ v ∈ B [n ← t] :: Δ'

(dependent evars:)





destruct v.
2 subgoals, subgoal 1 (ID 1655)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  H0 : S n > 0
  d : Term
  H1 : d ↓ 0 ∈ B :: Δ
  ============================
   d [(S n - 1) ← t] ↓ 0 ∈ B [n ← t] :: Δ'

subgoal 2 (ID 1660) is:
 d [(S n - S (S v)) ← t] ↓ S v ∈ B [n ← t] :: Δ'
(dependent evars:)





inversion H1; subst.
2 subgoals, subgoal 1 (ID 1729)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  H0 : S n > 0
  H1 : B ↓ 0 ∈ B :: Δ
  ============================
   B [(S n - 1) ← t] ↓ 0 ∈ B [n ← t] :: Δ'

subgoal 2 (ID 1660) is:
 d [(S n - S (S v)) ← t] ↓ S v ∈ B [n ← t] :: Δ'
(dependent evars:)





replace (S n -1) with n by intuition.
2 subgoals, subgoal 1 (ID 1733)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  H0 : S n > 0
  H1 : B ↓ 0 ∈ B :: Δ
  ============================
   B [n ← t] ↓ 0 ∈ B [n ← t] :: Δ'

subgoal 2 (ID 1660) is:
 d [(S n - S (S v)) ← t] ↓ S v ∈ B [n ← t] :: Δ'
(dependent evars:)





apply item_hd.
1 subgoals, subgoal 1 (ID 1660)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  ============================
   d [(S n - S (S v)) ← t] ↓ S v ∈ B [n ← t] :: Δ'

(dependent evars:)





replace (S n - S (S v)) with (n - S v) by intuition.
1 subgoals, subgoal 1 (ID 1752)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  ============================
   d [(n - S v) ← t] ↓ S v ∈ B [n ← t] :: Δ'

(dependent evars:)





inversion H1; subst.
1 subgoals, subgoal 1 (ID 1831)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d [(n - S v) ← t] ↓ S v ∈ B [n ← t] :: Δ'

(dependent evars:)





apply item_tl.
1 subgoals, subgoal 1 (ID 1832)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d [(n - S v) ← t] ↓ v ∈ Δ'

(dependent evars:)





apply gt_S_n in H0.
1 subgoals, subgoal 1 (ID 1834)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ← t] ↓ v ∈ Δ'
  v : nat
  H0 : n > v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d [(n - S v) ← t] ↓ v ∈ Δ'

(dependent evars:)





apply IHsub_in_env; trivial.
No more subgoals.
(dependent evars:)





Qed.
nth_sub_inf is defined








Lemma nth_sub_item_inf :

   forall t T n g e f , sub_in_env g t T n e f ->

   forall v : nat, n > v ->

   forall u , item_lift u e v -> item_lift (subst_rec t u n) f v.
1 subgoals, subgoal 1 (ID 1844)
  
  ============================
   forall (t T : Term) (n : nat) (g e f : Env),
   sub_in_env g t T n e f ->
   forall v : nat, n > v -> forall u : Term, u ↓ v ⊂ e -> u [n ← t] ↓ v ⊂ f

(dependent evars:)





intros.
1 subgoals, subgoal 1 (ID 1855)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  H1 : u ↓ v ⊂ e
  ============================
   u [n ← t] ↓ v ⊂ f

(dependent evars:)





destruct H1 as [y [K L]].
1 subgoals, subgoal 1 (ID 1863)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  y : Term
  K : u = y ↑ (S v)
  L : y ↓ v ∈ e
  ============================
   u [n ← t] ↓ v ⊂ f

(dependent evars:)





exists (subst_rec t y (n-S v)); split.
2 subgoals, subgoal 1 (ID 1867)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  y : Term
  K : u = y ↑ (S v)
  L : y ↓ v ∈ e
  ============================
   u [n ← t] = y [(n - S v) ← t] ↑ (S v)

subgoal 2 (ID 1868) is:
 y [(n - S v) ← t] ↓ v ∈ f
(dependent evars:)





rewrite K; clear u K.
2 subgoals, subgoal 1 (ID 1870)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  y : Term
  L : y ↓ v ∈ e
  ============================
   y ↑ (S v) [n ← t] = y [(n - S v) ← t] ↑ (S v)

subgoal 2 (ID 1868) is:
 y [(n - S v) ← t] ↓ v ∈ f
(dependent evars:)





pattern n at 1 .
2 subgoals, subgoal 1 (ID 1871)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  y : Term
  L : y ↓ v ∈ e
  ============================
   (fun n0 : nat => y ↑ (S v) [n0 ← t] = y [(n - S v) ← t] ↑ (S v)) n

subgoal 2 (ID 1868) is:
 y [(n - S v) ← t] ↓ v ∈ f
(dependent evars:)





replace n with (S v + ( n - S v)) by intuition.
2 subgoals, subgoal 1 (ID 1875)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  y : Term
  L : y ↓ v ∈ e
  ============================
   y ↑ (S v) [(S v + (n - S v)) ← t] = y [(n - S v) ← t] ↑ (S v)

subgoal 2 (ID 1868) is:
 y [(n - S v) ← t] ↓ v ∈ f
(dependent evars:)





apply substP2; intuition.
1 subgoals, subgoal 1 (ID 1868)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  y : Term
  K : u = y ↑ (S v)
  L : y ↓ v ∈ e
  ============================
   y [(n - S v) ← t] ↓ v ∈ f

(dependent evars:)





apply nth_sub_inf with T g  e; trivial.
No more subgoals.
(dependent evars:)





Qed.
nth_sub_item_inf is defined








End env_mod.
Module Type env_mod is defined
















Index
This page has been generated by coqdoc