# Typing Environment Definition and Function Manipulation.

Require Import base ut_term.

Require Import List.

Require Import Peano_dec.

Require Import Compare_dec.

Require Import Lt Le Gt.

Module Type ut_env_mod (X: term_sig) (TM: ut_term_mod X).
```Interactive Module Type ut_env_mod started

```

Import TM.

Since we use de Bruijn indexes, Environment (or Context) are simply lists of terms: Γ(x:A) is encoded as A::Γ.

Definition Env := list Term.
```Env is defined

```

Some manipulation functions (mostly from Bruno Barras' PTS contrib):
• how to find an item in the environment
• how to truncate an environment
• how to insert a new element (with correct de Bruijn update)
• how to substitute something in the environment
Set Implicit Arguments.

Inductive item (A:Type) (x:A): list A ->nat->Prop :=
| item_hd: forall Γ :list A, (item x (cons x Γ) O)
| item_tl: forall (Γ:list A)(n:nat)(y:A), item x Γ n -> item x (cons y Γ) (S n).
```item is defined
item_ind is defined

```

Hint Constructors item.

In the list Γ, the nth item is syntacticaly x.
Notation " x ↓ n ∈ Γ " := (item x Γ n) (at level 80, no associativity) : UT_scope.

Lemma fun_item: forall T (A B:T)(Γ:list T)(n:nat),
A n Γ -> B n Γ -> A = B.
```1 subgoals, subgoal 1 (ID 7)

============================
forall (T : Type) (A B : T) (Γ : list T) (n : nat),
A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B

(dependent evars:)

```

intros T A B Γ n;revert T A B Γ.
```1 subgoals, subgoal 1 (ID 14)

n : nat
============================
forall (T : Type) (A B : T) (Γ : list T), A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B

(dependent evars:)

```

induction n; intros.
```2 subgoals, subgoal 1 (ID 26)

T : Type
A : T
B : T
Γ : list T
H : A ↓ 0 ∈ Γ
H0 : B ↓ 0 ∈ Γ
============================
A = B

subgoal 2 (ID 32) is:
A = B
(dependent evars:)

```

inversion H; inversion H0.
```2 subgoals, subgoal 1 (ID 77)

T : Type
A : T
B : T
Γ : list T
H : A ↓ 0 ∈ Γ
H0 : B ↓ 0 ∈ Γ
Γ0 : list T
H1 : A :: Γ0 = Γ
Γ1 : list T
H2 : B :: Γ1 = Γ
============================
A = B

subgoal 2 (ID 32) is:
A = B
(dependent evars:)

```

rewrite <- H2 in H1; injection H1; trivial.
```1 subgoals, subgoal 1 (ID 32)

n : nat
IHn : forall (T : Type) (A B : T) (Γ : list T),
A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B
T : Type
A : T
B : T
Γ : list T
H : A ↓ S n ∈ Γ
H0 : B ↓ S n ∈ Γ
============================
A = B

(dependent evars:)

```

inversion H; inversion H0; subst.
```1 subgoals, subgoal 1 (ID 207)

n : nat
IHn : forall (T : Type) (A B : T) (Γ : list T),
A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B
T : Type
A : T
B : T
Γ0 : list T
y : T
H3 : A ↓ n ∈ Γ0
Γ1 : list T
y0 : T
H6 : B ↓ n ∈ Γ1
H : A ↓ S n ∈ y :: Γ0
H0 : B ↓ S n ∈ y :: Γ0
H5 : y0 :: Γ1 = y :: Γ0
============================
A = B

(dependent evars:)

```

injection H5; intros; subst.
```1 subgoals, subgoal 1 (ID 228)

n : nat
IHn : forall (T : Type) (A B : T) (Γ : list T),
A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B
T : Type
A : T
B : T
Γ0 : list T
y : T
H3 : A ↓ n ∈ Γ0
H : A ↓ S n ∈ y :: Γ0
H0 : B ↓ S n ∈ y :: Γ0
H6 : B ↓ n ∈ Γ0
H5 : y :: Γ0 = y :: Γ0
============================
A = B

(dependent evars:)

```

apply IHn with (Γ:=Γ0); 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 (T:Type) (n:nat) (Γ:list T) (t:T),
t n Γ -> exists Γ' , trunc (S n) Γ Γ'.
```1 subgoals, subgoal 1 (ID 236)

============================
forall (T : Type) (n : nat) (Γ : list T) (t : T),
t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'

(dependent evars:)

```

intros T n; induction n; intros.
```2 subgoals, subgoal 1 (ID 247)

T : Type
Γ : list T
t : T
H : t ↓ 0 ∈ Γ
============================
exists Γ' : list T, trunc 1 Γ Γ'

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

```

inversion H.
```2 subgoals, subgoal 1 (ID 265)

T : Type
Γ : list T
t : T
H : t ↓ 0 ∈ Γ
Γ0 : list T
H0 : t :: Γ0 = Γ
============================
exists Γ' : list T, trunc 1 (t :: Γ0) Γ'

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

```

exists Γ0.
```2 subgoals, subgoal 1 (ID 291)

T : Type
Γ : list T
t : T
H : t ↓ 0 ∈ Γ
Γ0 : list T
H0 : t :: Γ0 = Γ
============================
trunc 1 (t :: Γ0) Γ0

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

```

apply trunc_S; apply trunc_O.
```1 subgoals, subgoal 1 (ID 250)

T : Type
n : nat
IHn : forall (Γ : list T) (t : T),
t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
Γ : list T
t : T
H : t ↓ S n ∈ Γ
============================
exists Γ' : list T, trunc (S (S n)) Γ Γ'

(dependent evars:)

```

inversion H; subst.
```1 subgoals, subgoal 1 (ID 348)

T : Type
n : nat
IHn : forall (Γ : list T) (t : T),
t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
t : T
Γ0 : list T
y : T
H2 : t ↓ n ∈ Γ0
H : t ↓ S n ∈ y :: Γ0
============================
exists Γ' : list T, trunc (S (S n)) (y :: Γ0) Γ'

(dependent evars:)

```

destruct (IHn Γ0 t H2).
```1 subgoals, subgoal 1 (ID 355)

T : Type
n : nat
IHn : forall (Γ : list T) (t : T),
t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
t : T
Γ0 : list T
y : T
H2 : t ↓ n ∈ Γ0
H : t ↓ S n ∈ y :: Γ0
x : list T
H0 : trunc (S n) Γ0 x
============================
exists Γ' : list T, trunc (S (S n)) (y :: Γ0) Γ'

(dependent evars:)

```

exists x.
```1 subgoals, subgoal 1 (ID 357)

T : Type
n : nat
IHn : forall (Γ : list T) (t : T),
t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
t : T
Γ0 : list T
y : T
H2 : t ↓ n ∈ Γ0
H : t ↓ S n ∈ y :: Γ0
x : list T
H0 : trunc (S n) Γ0 x
============================
trunc (S (S n)) (y :: Γ0) x

(dependent evars:)

```

apply trunc_S.
```1 subgoals, subgoal 1 (ID 358)

T : Type
n : nat
IHn : forall (Γ : list T) (t : T),
t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
t : T
Γ0 : list T
y : T
H2 : t ↓ n ∈ Γ0
H : t ↓ S n ∈ y :: Γ0
x : list T
H0 : trunc (S n) Γ0 x
============================
trunc (S n) Γ0 x

(dependent evars:)

```

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

```

Qed.
```item_trunc is defined

```

This type describe how do we add an element in an environment: no type checking is done, this is just the mecanic way to do it.
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.

Some lemmas about inserting a new element. They explain how terms in the environment are lifted according to their original position and the position of insertion.
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)
Γ0 : list Term
n0 : nat
y : Term
H4 : d ↓ v ∈ Δ0
H2 : y = d0
H5 : Γ0 = Δ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)
Γ0 : list Term
n0 : nat
y : Term
H4 : d ↓ v ∈ Δ0
H2 : y = d0
H5 : Γ0 = Δ0
H6 : n0 = v
============================
d ↓ v ∈ Δ0

(dependent evars:)

```

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

```

Qed.
```ins_item_lt is defined

```

In the list Γ, t is nth element correctly lifted according to Γ: e.g.: if t ↓ n ⊂ Γ and we insert something in Γ, then we can still speak about t without think of the lift hidden by the insertion.

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): UT_scope.

Properties of the item_lift notation.
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

```

This type describe how do we do substitution inside a context. As previously, no type checking is done at this point.

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.

Some ins / subst related facts: what happens to term when we do a substitution in a context.
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 ut_env_mod.
```Module Type ut_env_mod is defined

```

Index