Library f_term

Term definition for PTSf and de Bruijn manipulation .

Require Import base.

Require Import List Lt Le Gt Plus Minus Peano_dec Compare_dec.

Interactive Module Type f_term_mod started

Import X.

Term syntax, extended with convertibility proofs .

Term, Prf are defined
Term_rect is defined
Term_ind is defined
Term_rec is defined
Prf_rect is defined
Prf_ind is defined
Prf_rec is defined

Notation "! s" := (Sort s) (at level 1) : F_scope.

Notation "# v" := (Var v) (at level 1) : F_scope.

Notation "'Π' ( U ) , V " := (Prod U V) (at level 20, U, V at level 30) : F_scope.

Identifier 'Π' now a keyword

Notation "'λ' [ U ] , v " := (Abs U v) (at level 20, U , v at level 30) : F_scope.

Identifier 'λ' now a keyword

Notation "x · y" := (App x y) (at level 15, left associativity) : F_scope.

Notation "A ∽ H" := (Conv A H) (at level 15) : F_scope.

Notation "'ρ' A" := (Refl A) (at level 6) : F_scope.

Identifier 'ρ' now a keyword

Notation "H †" := (Sym H) (at level 6) : F_scope.

Notation "H1 • H2" := (Trans H1 H2) (at level 15, left associativity) : F_scope.

Notation "'β' A" := (Beta A) (at level 6) : F_scope.

Identifier 'β' now a keyword

Notation "{ H1 , [ A ] H2 }" := (ProdEq H1 A H2) (at level 15) : F_scope.

Notation "⟨ H1 , [ A ] H2 ⟩" := (AbsEq H1 A H2) (at level 15, left associativity) : F_scope.

Notation "H1 ·h H2" := (AppEq H1 H2) (at level 15, left associativity) : F_scope.

Notation "'ι' A" := (Iota A) (at level 6) : F_scope.

Identifier 'ι' now a keyword

Reserved Notation " t ↑ x # n " (at level 5, x at level 0, left associativity).

Reserved Notation " t ↑h x # n " (at level 5, x at level 0, left associativity).

Delimit Scope F_scope with F.

Open Scope F_scope.

Scheme Term_ind' := Induction for Term Sort Prop
with Prf_ind' := Induction for Prf Sort Prop.

Prf_ind' is defined
Term_ind' is defined
Term_ind', Prf_ind' are recursively defined

Combined Scheme Term_induc from Term_ind', Prf_ind'.

Term_induc is defined
Term_induc is recursively defined

In order to deal with variable bindings and captures, we need a lift function to deal with free and bounded variables.

M ↑ n m recursivly adds n to all variables that are above m in M. H ↑h n m does the same for convertibility proofs

Fixpoint lift_rec (n:nat) (k:nat) (T:Term) {struct T} := match T with
   | # x => if le_gt_dec k x then Var (n +x) else Var x
   | ! s => Sort s
   | M · N => App (M ↑ n # k) (N ↑ n # k)
   | Π ( A ), B => Π (A ↑ n # k ), (B ↑ n # (S k ))
   | λ [ A ], M => λ [A ↑ n # k ], (M ↑ n # (S k ))
   | A ∽ H => A ↑ n # k ∽ H ↑h n # k
end
   where "t ↑ n # k" := (lift_rec n k t) : F_scope
with lift_rec_h (n:nat) (k:nat) (H:Prf) {struct H} := match H with
   | ρ A => ρ (A ↑ n # k )
   | H† => (H ↑h n # k )†
   | H•K => (H ↑h n # k )•(K ↑h n # k )
   | β A => β (A ↑ n # k )
   | H ·h K => (H ↑h n # k ) ·h (K ↑h n # k )
   | {H,[A]K} => {H ↑h n # k ,[A ↑ n # k ]K ↑h n # (S k )}
   | ⟨H,[A]K⟩ => ⟨H ↑h n # k ,[A ↑ n # k ]K ↑h n # (S k )⟩
   | ι A => ι (A ↑ n # k )
end
where "t ↑h n # k" := (lift_rec_h n k t) : F_scope.

lift_rec, lift_rec_h are recursively defined (decreasing respectively on 3rd,
3rd arguments)

Notation " t ↑ n " := (lift_rec n 0 t) (at level 5, n at level 0, left associativity) : F_scope.

Notation " t ↑h n " := (lift_rec_h n 0 t) (at level 5, n at level 0, left associativity) : F_scope.

Some basic properties of the lift function. That is everything we will ever need to handle de Bruijn indexes

Lemma inv_lift : (forall M N n m, M ↑ n # m = N ↑ n # m -> M = N ) /\
(forall M N n m, M ↑h n # m = N ↑h n # m -> M = N ).

1 subgoals, subgoal 1 (ID 16)
  
  ============================
   (forall (M N : Term) (n m : nat), M ↑  n # m = N ↑  n # m -> M = N) /\
   (forall (M N : Prf) (n m : nat), M ↑h n # m = N ↑h n # m -> M = N)

(dependent evars:)

apply Term_induc;try destruct N;try destruct K;intros;simpl in *;

try discriminate;try intuition;

(try (destruct (le_gt_dec m v) ; discriminate));

try (injection H2;intros;rewrite (H N1 n m H5);rewrite (H0 t0 n m H4);rewrite (H1 N2 n (S m) H3);reflexivity);

try (injection H1;intros;rewrite (H N1 n m H3)||rewrite (H N n m H3);rewrite (H0 N2 n m H2)
||rewrite (H0 N2 n (S m) H2)||rewrite (H0 p0 n m H2);reflexivity);

try (injection H0;intros;rewrite (H t0 n m H1)||rewrite (H N n m H1);reflexivity).

1 subgoals, subgoal 1 (ID 768)
  
  v : Vars
  v0 : Vars
  n : nat
  m : nat
  H : (if le_gt_dec m v then #(n + v) else #v) =
      (if le_gt_dec m v0 then #(n + v0) else #v0)
  ============================
   #v = #v0

(dependent evars:)

destruct (le_gt_dec m v); destruct (le_gt_dec m v0); injection H; intros; subst; intuition.

3 subgoals, subgoal 1 (ID 2807)
  
  v : Vars
  v0 : Vars
  n : nat
  m : nat
  l : m <= v
  l0 : m <= v0
  H : #(n + v) = #(n + v0)
  H0 : n + v = n + v0
  ============================
   #v = #v0

subgoal 2 (ID 2816) is:
 #v = #(n + v)
subgoal 3 (ID 2822) is:
 #(n + v0) = #v0
(dependent evars:)

apply plus_reg_l in H0; rewrite H0; trivial.

2 subgoals, subgoal 1 (ID 2816)
  
  v : Vars
  n : nat
  m : nat
  l : m <= v
  g : m > n + v
  H : #(n + v) = #(n + v)
  ============================
   #v = #(n + v)

subgoal 2 (ID 2822) is:
 #(n + v0) = #v0
(dependent evars:)

elim (lt_irrefl m).

2 subgoals, subgoal 1 (ID 2895)
  
  v : Vars
  n : nat
  m : nat
  l : m <= v
  g : m > n + v
  H : #(n + v) = #(n + v)
  ============================
   m < m

subgoal 2 (ID 2822) is:
 #(n + v0) = #v0
(dependent evars:)

apply le_lt_trans with v.

3 subgoals, subgoal 1 (ID 2896)
  
  v : Vars
  n : nat
  m : nat
  l : m <= v
  g : m > n + v
  H : #(n + v) = #(n + v)
  ============================
   m <= v

subgoal 2 (ID 2897) is:
 v < m
subgoal 3 (ID 2822) is:
 #(n + v0) = #v0
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 2897)
  
  v : Vars
  n : nat
  m : nat
  l : m <= v
  g : m > n + v
  H : #(n + v) = #(n + v)
  ============================
   v < m

subgoal 2 (ID 2822) is:
 #(n + v0) = #v0
(dependent evars:)

induction n; intuition.

1 subgoals, subgoal 1 (ID 2822)
  
  v0 : Vars
  n : nat
  m : nat
  l : m <= v0
  g : m > n + v0
  H : #(n + v0) = #(n + v0)
  ============================
   #(n + v0) = #v0

(dependent evars:)

elim (lt_irrefl v0).

1 subgoals, subgoal 1 (ID 2935)
  
  v0 : Vars
  n : nat
  m : nat
  l : m <= v0
  g : m > n + v0
  H : #(n + v0) = #(n + v0)
  ============================
   v0 < v0

(dependent evars:)

apply lt_le_trans with m.

2 subgoals, subgoal 1 (ID 2936)
  
  v0 : Vars
  n : nat
  m : nat
  l : m <= v0
  g : m > n + v0
  H : #(n + v0) = #(n + v0)
  ============================
   v0 < m

subgoal 2 (ID 2937) is:
 m <= v0
(dependent evars:)

induction n; intuition.

1 subgoals, subgoal 1 (ID 2937)
  
  v0 : Vars
  n : nat
  m : nat
  l : m <= v0
  g : m > n + v0
  H : #(n + v0) = #(n + v0)
  ============================
   m <= v0

(dependent evars:)

trivial.

No more subgoals.
(dependent evars:)

Qed.

inv_lift is defined

Lemma lift_rec0 : (forall M n, M ↑ 0 # n = M ) /\ (forall H n, H ↑h 0 # n = H ).

1 subgoals, subgoal 1 (ID 2981)
  
  ============================
   (forall (M : Term) (n : nat), M ↑  0 # n = M) /\
   (forall (H : Prf) (n : nat), H ↑h 0 # n = H)

(dependent evars:)

apply Term_induc;intros;simpl;try rewrite H;try rewrite H0;try rewrite H1;try rewrite H2;try reflexivity.

1 subgoals, subgoal 1 (ID 3056)
  
  v : Vars
  n : nat
  ============================
   (if le_gt_dec n v then #v else #v) = #v

(dependent evars:)

destruct (le_gt_dec n v); reflexivity.

No more subgoals.
(dependent evars:)

Qed.

lift_rec0 is defined

Lemma lift0 : (forall M, M ↑ 0 = M ) /\ (forall H, H ↑h 0 = H ).

1 subgoals, subgoal 1 (ID 3122)
  
  ============================
   (forall M : Term, M ↑  0 = M) /\ (forall H : Prf, H ↑h 0 = H)

(dependent evars:)

destruct lift_rec0; intuition.

No more subgoals.
(dependent evars:)

Qed.

lift0 is defined

Lemma liftP1 : (forall M i j k, (M ↑ j # i ) ↑ k # (j +i ) = M ↑ (j +k ) # i ) /\
(forall H i j k, (H ↑h j # i ) ↑h k # (j +i ) = H ↑h (j +k ) # i ).

1 subgoals, subgoal 1 (ID 3155)
  
  ============================
   (forall (M : Term) (i j k : nat),
    M ↑  j # i ↑  k # (j + i) = M ↑  (j + k) # i) /\
   (forall (H : Prf) (i j k : nat),
    H ↑h j # i ↑h k # (j + i) = H ↑h (j + k) # i)

(dependent evars:)

apply Term_induc;intros;simpl;try rewrite <- H;try rewrite <- H0; try rewrite <- H1;
try (replace (j+S i) with (S(j+i)) by intuition);try reflexivity.

1 subgoals, subgoal 1 (ID 3296)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  ============================
   (if le_gt_dec i v then #(j + v) else #v) ↑  k # (j + i) =
   (if le_gt_dec i v then #(j + k + v) else #v)

(dependent evars:)

destruct le_gt_dec;simpl;destruct le_gt_dec;
try (rewrite plus_assoc;replace (k+j) with (j+k) by (apply plus_comm));try reflexivity.

2 subgoals, subgoal 1 (ID 3533)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  l : i <= v
  g : j + i > j + v
  ============================
   #(j + v) = #(j + k + v)

subgoal 2 (ID 3542) is:
 #(k + v) = #v
(dependent evars:)

apply plus_gt_reg_l in g.

2 subgoals, subgoal 1 (ID 3555)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  l : i <= v
  g : i > v
  ============================
   #(j + v) = #(j + k + v)

subgoal 2 (ID 3542) is:
 #(k + v) = #v
(dependent evars:)

elim (lt_irrefl v).

2 subgoals, subgoal 1 (ID 3556)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  l : i <= v
  g : i > v
  ============================
   v < v

subgoal 2 (ID 3542) is:
 #(k + v) = #v
(dependent evars:)

apply lt_le_trans with i; intuition.

1 subgoals, subgoal 1 (ID 3542)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  g : i > v
  l : j + i <= v
  ============================
   #(k + v) = #v

(dependent evars:)

elim (lt_irrefl v).

1 subgoals, subgoal 1 (ID 3559)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  g : i > v
  l : j + i <= v
  ============================
   v < v

(dependent evars:)

apply lt_le_trans with i; intuition.

1 subgoals, subgoal 1 (ID 3561)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  g : i > v
  l : j + i <= v
  ============================
   i <= v

(dependent evars:)

induction j; intuition.

No more subgoals.
(dependent evars:)

Qed.

liftP1 is defined

Lemma liftP2: (forall M i j k n, i <= n -> (M ↑ j # i ) ↑ k # (j +n ) = (M ↑ k # n ) ↑ j # i )/\
(forall H i j k n, i <= n -> (H ↑h j # i ) ↑h k # (j +n ) = (H ↑h k # n ) ↑h j # i ).

1 subgoals, subgoal 1 (ID 3614)
  
  ============================
   (forall (M : Term) (i j k n : nat),
    i <= n -> M ↑  j # i ↑  k # (j + n) = M ↑  k # n ↑  j # i) /\
   (forall (H : Prf) (i j k n : nat),
    i <= n -> H ↑h j # i ↑h k # (j + n) = H ↑h k # n ↑h j # i)

(dependent evars:)

apply Term_induc;intros;simpl;try replace (S(j+n)) with (j+S n) by intuition;
try rewrite H by intuition;try rewrite H0 by intuition;try rewrite H1 by intuition;try reflexivity.

1 subgoals, subgoal 1 (ID 3761)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  ============================
   (if le_gt_dec i v then #(j + v) else #v) ↑  k # (j + n) =
   (if le_gt_dec n v then #(k + v) else #v) ↑  j # i

(dependent evars:)

destruct (le_gt_dec i v); destruct (le_gt_dec n v); simpl;destruct le_gt_dec;destruct le_gt_dec;try intuition;
[|elim (lt_irrefl v); try (apply lt_le_trans with i;trivial;try (apply le_trans with n;trivial;fail);fail);
try (try (apply plus_gt_reg_l in g);try (apply plus_le_reg_l in l0); try (apply le_trans with n;trivial);fail)..].

3 subgoals, subgoal 1 (ID 6403)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n <= v
  l1 : j + n <= j + v
  l2 : i <= k + v
  ============================
   #(k + (j + v)) = #(j + (k + v))

subgoal 2 (ID 6902) is:
 v < v
subgoal 3 (ID 6960) is:
 v < v
(dependent evars:)

rewrite 2! plus_assoc.

3 subgoals, subgoal 1 (ID 6971)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n <= v
  l1 : j + n <= j + v
  l2 : i <= k + v
  ============================
   #(k + j + v) = #(j + k + v)

subgoal 2 (ID 6902) is:
 v < v
subgoal 3 (ID 6960) is:
 v < v
(dependent evars:)

replace (k+j) with (j+k) by (apply plus_comm).

3 subgoals, subgoal 1 (ID 6975)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n <= v
  l1 : j + n <= j + v
  l2 : i <= k + v
  ============================
   #(j + k + v) = #(j + k + v)

subgoal 2 (ID 6902) is:
 v < v
subgoal 3 (ID 6960) is:
 v < v
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 6902)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n <= v
  l1 : j + n <= j + v
  g : i > k + v
  ============================
   v < v

subgoal 2 (ID 6960) is:
 v < v
(dependent evars:)

apply lt_le_trans with i;trivial.

2 subgoals, subgoal 1 (ID 6977)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n <= v
  l1 : j + n <= j + v
  g : i > k + v
  ============================
   v < i

subgoal 2 (ID 6960) is:
 v < v
(dependent evars:)

induction k; intuition.

1 subgoals, subgoal 1 (ID 6960)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  g : i > v
  g0 : n > v
  l : j + n <= v
  g1 : i > v
  ============================
   v < v

(dependent evars:)

apply lt_le_trans with n;intuition.

1 subgoals, subgoal 1 (ID 7017)
  
  v : Vars
  i : nat
  j : nat
  k : nat
  n : nat
  H : i <= n
  g : i > v
  g0 : n > v
  l : j + n <= v
  g1 : i > v
  ============================
   n <= v

(dependent evars:)

induction l;intuition.

No more subgoals.
(dependent evars:)

Qed.

liftP2 is defined

Lemma liftP3 : (forall M i k j n , i <= k -> k <= (i +n ) -> (M ↑ n # i ) ↑ j # k = M ↑ (j +n ) # i ) /\
(forall H i k j n , i <= k -> k <= (i +n ) -> (H ↑h n # i ) ↑h j # k = H ↑h (j +n ) # i ).

1 subgoals, subgoal 1 (ID 7130)
  
  ============================
   (forall (M : Term) (i k j n : nat),
    i <= k -> k <= i + n -> M ↑  n # i ↑  j # k = M ↑  (j + n) # i) /\
   (forall (H : Prf) (i k j n : nat),
    i <= k -> k <= i + n -> H ↑h n # i ↑h j # k = H ↑h (j + n) # i)

(dependent evars:)

apply Term_induc;intros;simpl;
try rewrite H; intuition; try rewrite H0; intuition; try rewrite H1;intuition;
try change (S i+n) with (S(i+n));intuition.

1 subgoals, subgoal 1 (ID 9117)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  ============================
   (if le_gt_dec i v then #(n + v) else #v) ↑  j # k =
   (if le_gt_dec i v then #(j + n + v) else #v)

(dependent evars:)

destruct (le_gt_dec i v); simpl.

2 subgoals, subgoal 1 (ID 9203)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  ============================
   (if le_gt_dec k (n + v) then #(j + (n + v)) else #(n + v)) = #(j + n + v)

subgoal 2 (ID 9204) is:
 (if le_gt_dec k v then #(j + v) else #v) = #v
(dependent evars:)

destruct (le_gt_dec k (n+v)); intuition.

2 subgoals, subgoal 1 (ID 9214)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  g : k > n + v
  ============================
   #(n + v) = #(j + n + v)

subgoal 2 (ID 9204) is:
 (if le_gt_dec k v then #(j + v) else #v) = #v
(dependent evars:)

elim (lt_irrefl (i+n)).

2 subgoals, subgoal 1 (ID 9262)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  g : k > n + v
  ============================
   i + n < i + n

subgoal 2 (ID 9204) is:
 (if le_gt_dec k v then #(j + v) else #v) = #v
(dependent evars:)

apply lt_le_trans with k;trivial.

2 subgoals, subgoal 1 (ID 9263)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  g : k > n + v
  ============================
   i + n < k

subgoal 2 (ID 9204) is:
 (if le_gt_dec k v then #(j + v) else #v) = #v
(dependent evars:)

apply le_lt_trans with (n+v);trivial.

2 subgoals, subgoal 1 (ID 9265)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  g : k > n + v
  ============================
   i + n <= n + v

subgoal 2 (ID 9204) is:
 (if le_gt_dec k v then #(j + v) else #v) = #v
(dependent evars:)

rewrite plus_comm;intuition.

1 subgoals, subgoal 1 (ID 9204)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  ============================
   (if le_gt_dec k v then #(j + v) else #v) = #v

(dependent evars:)

destruct (le_gt_dec k v); intuition.

1 subgoals, subgoal 1 (ID 9294)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : k <= v
  ============================
   #(j + v) = #v

(dependent evars:)

elim (lt_irrefl k).

1 subgoals, subgoal 1 (ID 9320)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : k <= v
  ============================
   k < k

(dependent evars:)

apply lt_le_trans with i;trivial.

1 subgoals, subgoal 1 (ID 9321)
  
  v : Vars
  i : nat
  k : nat
  j : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : k <= v
  ============================
   k < i

(dependent evars:)

apply le_lt_trans with v;intuition.

No more subgoals.
(dependent evars:)

Qed.

liftP3 is defined

Lemma lift_lift : (forall M n m, (M ↑ m ) ↑ n = M ↑ (n +m )) /\
(forall H n m, (H ↑h m ) ↑h n = H ↑h (n +m )).

1 subgoals, subgoal 1 (ID 9333)
  
  ============================
   (forall (M : Term) (n m : nat), M ↑  m ↑  n = M ↑  (n + m)) /\
   (forall (H : Prf) (n m : nat), H ↑h m ↑h n = H ↑h (n + m))

(dependent evars:)

destruct liftP3;intuition.

No more subgoals.
(dependent evars:)

Qed.

lift_lift is defined

We will consider the usual implicit substitution without variable capture (this is where the lift operator comes in handy).

M n ← N replaces the variable n in M by the term N and M n ←h N does the same for convertibility proofs.

Reserved Notation "t [ x ← u ]" (at level 5, x at level 0, left associativity).

Reserved Notation "t [ x ←h u ]" (at level 5, x at level 0, left associativity).

Fixpoint subst_rec U T n {struct T} :=
match T with
   | # x => match (lt_eq_lt_dec x n) with
      | inleft (left _) => # x
      | inleft (right _) => U ↑ n
      | inright _ => # (x - 1)
      end
   | ! s => ! s
   | M · N => (M [ n ← U ]) · ( N [ n ← U ])
   | Π ( A ), B => Π ( A [ n ← U ] ), (B [ S n ← U ])
   | λ [ A ], M => λ [ A [ n ← U ] ], (M [ S n ← U ])
   | A ∽ H => A [ n ← U ] ∽ H [ n ←h U ]
end
      where " t [ n ← w ] " := (subst_rec w t n) : F_scope
with subst_rec_h U H n {struct H} := match H with
   | ρ A => ρ A [ n ← U ]
   | H† => H [ n ←h U ] †
   | H•K => H [ n ←h U ]•K[ n ←h U ]
   | β A => β A[ n ← U ]
   | H ·h K => H [ n ←h U ] ·h K[ n ←h U ]
   | {H,[A]K} => {H [ n ←h U ],[A[ n ← U ]]K[ S n ←h U ]}
   | ⟨H,[A]K⟩ => ⟨H [ n ←h U ],[A[ n ← U ]]K[ S n ←h U ]⟩
   | ι A => ι A [ n ← U ]
end
      where " t [ n ←h w ] " := (subst_rec_h w t n) : F_scope.

subst_rec, subst_rec_h are recursively defined
(decreasing respectively on 2nd, 2nd arguments)

Notation " t [ ← w ] " := (subst_rec w t 0) (at level 5) : F_scope.

Notation " t [ ←h w ] " := (subst_rec_h w t 0) (at level 5) : F_scope.

Some basic properties of the substitution function. Again, we will only need a few functions to deal with indexes.

Lemma substP1: (forall M N i j k, ( M [ j ← N ] ) ↑ k # (j +i ) = (M ↑ k # (S (j +i))) [ j ← (N ↑ k # i ) ])/\
(forall H N i j k, ( H [ j ←h N ] ) ↑h k # (j +i ) = (H ↑h k # (S (j +i))) [ j ←h (N ↑ k # i ) ]).

1 subgoals, subgoal 1 (ID 9390)
  
  ============================
   (forall (M N : Term) (i j k : nat),
    M [j ←  N] ↑  k # (j + i) = M ↑  k # (S (j + i)) [j ←  N ↑  k # i]) /\
   (forall (H : Prf) (N : Term) (i j k : nat),
    H [j ←h N] ↑h k # (j + i) = H ↑h k # (S (j + i)) [j ←h N ↑  k # i])

(dependent evars:)

apply Term_induc;intros;
[|simpl;
try replace (S(S(j+i))) with (S((S j)+i)) by intuition;
try rewrite H; intuition; try rewrite H0; intuition;
try rewrite <- (H0 N i (S j) k );try rewrite <- (H1 N i (S j) k);intuition..].

1 subgoals, subgoal 1 (ID 9409)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  ============================
   #v [j ←  N] ↑  k # (j + i) = #v ↑  k # (S (j + i)) [j ←  N ↑  k # i]

(dependent evars:)

simpl (#v [j ← N] ↑ k # (j+i)).

1 subgoals, subgoal 1 (ID 9776)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  ============================
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  j
   | inright _ => #(v - 1)
   end ↑  k # (j + i) = #v ↑  k # (S (j + i)) [j ←  N ↑  k # i]

(dependent evars:)

change (#v ↑ k # (S (j+i))) with (if le_gt_dec (S (j+i)) v then #(k+v) else #v).

1 subgoals, subgoal 1 (ID 9779)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  ============================
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  j
   | inright _ => #(v - 1)
   end ↑  k # (j + i) =
   (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]

(dependent evars:)

destruct (lt_eq_lt_dec v j) as [[] | ].

3 subgoals, subgoal 1 (ID 9793)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  ============================
   #v ↑  k # (j + i) =
   (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]

subgoal 2 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

destruct (le_gt_dec (S (j+i)) v).

4 subgoals, subgoal 1 (ID 9804)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  l0 : S (j + i) <= v
  ============================
   #v ↑  k # (j + i) = #(k + v) [j ←  N ↑  k # i]

subgoal 2 (ID 9805) is:
 #v ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl v).

4 subgoals, subgoal 1 (ID 9806)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  l0 : S (j + i) <= v
  ============================
   v < v

subgoal 2 (ID 9805) is:
 #v ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

apply lt_le_trans with j; intuition.

4 subgoals, subgoal 1 (ID 9808)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  l0 : S (j + i) <= v
  ============================
   j <= v

subgoal 2 (ID 9805) is:
 #v ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

apply le_trans with (S (j+i)); intuition.

3 subgoals, subgoal 1 (ID 9805)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  ============================
   #v ↑  k # (j + i) = #v [j ←  N ↑  k # i]

subgoal 2 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

simpl.

3 subgoals, subgoal 1 (ID 9843)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  ============================
   (if le_gt_dec (j + i) v then #(k + v) else #v) =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

destruct (le_gt_dec (j+i) v).

4 subgoals, subgoal 1 (ID 9852)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  l0 : j + i <= v
  ============================
   #(k + v) =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 9853) is:
 #v =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl v).

4 subgoals, subgoal 1 (ID 9854)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  l0 : j + i <= v
  ============================
   v < v

subgoal 2 (ID 9853) is:
 #v =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

apply lt_le_trans with j; intuition.

4 subgoals, subgoal 1 (ID 9856)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  l0 : j + i <= v
  ============================
   j <= v

subgoal 2 (ID 9853) is:
 #v =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

apply le_trans with (j+i); intuition.

3 subgoals, subgoal 1 (ID 9853)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  g0 : j + i > v
  ============================
   #v =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

destruct (lt_eq_lt_dec v j) as [[] | ].

5 subgoals, subgoal 1 (ID 9900)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  g0 : j + i > v
  l0 : v < j
  ============================
   #v = #v

subgoal 2 (ID 9901) is:
 #v = N ↑  k # i ↑  j
subgoal 3 (ID 9902) is:
 #v = #(v - 1)
subgoal 4 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 5 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

trivial.

4 subgoals, subgoal 1 (ID 9901)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  g0 : j + i > v
  e : v = j
  ============================
   #v = N ↑  k # i ↑  j

subgoal 2 (ID 9902) is:
 #v = #(v - 1)
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

subst.

4 subgoals, subgoal 1 (ID 9909)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < j
  g : S (j + i) > j
  g0 : j + i > j
  ============================
   #j = N ↑  k # i ↑  j

subgoal 2 (ID 9902) is:
 #v = #(v - 1)
subgoal 3 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl j);trivial.

3 subgoals, subgoal 1 (ID 9902)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : v < j
  g : S (j + i) > v
  g0 : j + i > v
  l0 : j < v
  ============================
   #v = #(v - 1)

subgoal 2 (ID 9794) is:
 N ↑  j ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl j); apply lt_trans with v; trivial.

2 subgoals, subgoal 1 (ID 9794)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  ============================
   N ↑  j ↑  k # (j + i) =
   (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]

subgoal 2 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

destruct (le_gt_dec (S(j+i)) v).

3 subgoals, subgoal 1 (ID 9922)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  l : S (j + i) <= v
  ============================
   N ↑  j ↑  k # (j + i) = #(k + v) [j ←  N ↑  k # i]

subgoal 2 (ID 9923) is:
 N ↑  j ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

subst.

3 subgoals, subgoal 1 (ID 9928)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : S (j + i) <= j
  ============================
   N ↑  j ↑  k # (j + i) = #(k + j) [j ←  N ↑  k # i]

subgoal 2 (ID 9923) is:
 N ↑  j ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl j).

3 subgoals, subgoal 1 (ID 9929)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : S (j + i) <= j
  ============================
   j < j

subgoal 2 (ID 9923) is:
 N ↑  j ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

apply lt_le_trans with (S (j+i)).

4 subgoals, subgoal 1 (ID 9930)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : S (j + i) <= j
  ============================
   j < S (j + i)

subgoal 2 (ID 9931) is:
 S (j + i) <= j
subgoal 3 (ID 9923) is:
 N ↑  j ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

intuition.

3 subgoals, subgoal 1 (ID 9931)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : S (j + i) <= j
  ============================
   S (j + i) <= j

subgoal 2 (ID 9923) is:
 N ↑  j ↑  k # (j + i) = #v [j ←  N ↑  k # i]
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 9923)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  g : S (j + i) > v
  ============================
   N ↑  j ↑  k # (j + i) = #v [j ←  N ↑  k # i]

subgoal 2 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

simpl.

2 subgoals, subgoal 1 (ID 9974)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  g : S (j + i) > v
  ============================
   N ↑  j ↑  k # (j + i) =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

destruct (lt_eq_lt_dec v j) as [[] | ].

4 subgoals, subgoal 1 (ID 9988)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  g : S (j + i) > v
  l : v < j
  ============================
   N ↑  j ↑  k # (j + i) = #v

subgoal 2 (ID 9989) is:
 N ↑  j ↑  k # (j + i) = N ↑  k # i ↑  j
subgoal 3 (ID 9990) is:
 N ↑  j ↑  k # (j + i) = #(v - 1)
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

subst.

4 subgoals, subgoal 1 (ID 9996)
  
  N : Term
  i : nat
  j : nat
  k : nat
  g : S (j + i) > j
  l : j < j
  ============================
   N ↑  j ↑  k # (j + i) = #j

subgoal 2 (ID 9989) is:
 N ↑  j ↑  k # (j + i) = N ↑  k # i ↑  j
subgoal 3 (ID 9990) is:
 N ↑  j ↑  k # (j + i) = #(v - 1)
subgoal 4 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl j); trivial.

3 subgoals, subgoal 1 (ID 9989)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  g : S (j + i) > v
  e0 : v = j
  ============================
   N ↑  j ↑  k # (j + i) = N ↑  k # i ↑  j

subgoal 2 (ID 9990) is:
 N ↑  j ↑  k # (j + i) = #(v - 1)
subgoal 3 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

apply liftP2; intuition.

2 subgoals, subgoal 1 (ID 9990)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  e : v = j
  g : S (j + i) > v
  l : j < v
  ============================
   N ↑  j ↑  k # (j + i) = #(v - 1)

subgoal 2 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 10018)
  
  N : Term
  i : nat
  j : nat
  k : nat
  g : S (j + i) > j
  l : j < j
  ============================
   N ↑  j ↑  k # (j + i) = #(j - 1)

subgoal 2 (ID 9795) is:
 #(v - 1) ↑  k # (j + i) =
 (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl j); trivial.

1 subgoals, subgoal 1 (ID 9795)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  ============================
   #(v - 1) ↑  k # (j + i) =
   (if le_gt_dec (S (j + i)) v then #(k + v) else #v) [j ←  N ↑  k # i]

(dependent evars:)

destruct (le_gt_dec (S (j+i)) v).

2 subgoals, subgoal 1 (ID 10028)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  ============================
   #(v - 1) ↑  k # (j + i) = #(k + v) [j ←  N ↑  k # i]

subgoal 2 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

simpl.

2 subgoals, subgoal 1 (ID 10030)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  ============================
   (if le_gt_dec (j + i) (v - 1) then #(k + (v - 1)) else #(v - 1)) =
   match lt_eq_lt_dec (k + v) j with
   | inleft (left _) => #(k + v)
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(k + v - 1)
   end

subgoal 2 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

destruct (le_gt_dec (j+i) (v-1)).

3 subgoals, subgoal 1 (ID 10039)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  ============================
   #(k + (v - 1)) =
   match lt_eq_lt_dec (k + v) j with
   | inleft (left _) => #(k + v)
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(k + v - 1)
   end

subgoal 2 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

destruct (lt_eq_lt_dec (k+v) j) as [[] | ].

5 subgoals, subgoal 1 (ID 10054)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  l2 : k + v < j
  ============================
   #(k + (v - 1)) = #(k + v)

subgoal 2 (ID 10055) is:
 #(k + (v - 1)) = N ↑  k # i ↑  j
subgoal 3 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 4 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 5 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl j).

5 subgoals, subgoal 1 (ID 10057)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  l2 : k + v < j
  ============================
   j < j

subgoal 2 (ID 10055) is:
 #(k + (v - 1)) = N ↑  k # i ↑  j
subgoal 3 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 4 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 5 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

apply lt_le_trans with v.

6 subgoals, subgoal 1 (ID 10058)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  l2 : k + v < j
  ============================
   j < v

subgoal 2 (ID 10059) is:
 v <= j
subgoal 3 (ID 10055) is:
 #(k + (v - 1)) = N ↑  k # i ↑  j
subgoal 4 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 5 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 6 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

trivial.

5 subgoals, subgoal 1 (ID 10059)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  l2 : k + v < j
  ============================
   v <= j

subgoal 2 (ID 10055) is:
 #(k + (v - 1)) = N ↑  k # i ↑  j
subgoal 3 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 4 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 5 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

induction k; intuition.

4 subgoals, subgoal 1 (ID 10055)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  e : k + v = j
  ============================
   #(k + (v - 1)) = N ↑  k # i ↑  j

subgoal 2 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 3 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 4 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

subst.

4 subgoals, subgoal 1 (ID 10113)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  l : k + v < v
  l0 : S (k + v + i) <= v
  l1 : k + v + i <= v - 1
  ============================
   #(k + (v - 1)) = N ↑  k # i ↑  (k + v)

subgoal 2 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 3 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 4 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl v).

4 subgoals, subgoal 1 (ID 10114)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  l : k + v < v
  l0 : S (k + v + i) <= v
  l1 : k + v + i <= v - 1
  ============================
   v < v

subgoal 2 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 3 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 4 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

apply lt_le_trans with (S(k+v+i)).

5 subgoals, subgoal 1 (ID 10115)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  l : k + v < v
  l0 : S (k + v + i) <= v
  l1 : k + v + i <= v - 1
  ============================
   v < S (k + v + i)

subgoal 2 (ID 10116) is:
 S (k + v + i) <= v
subgoal 3 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 4 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 5 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

intuition.

4 subgoals, subgoal 1 (ID 10116)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  l : k + v < v
  l0 : S (k + v + i) <= v
  l1 : k + v + i <= v - 1
  ============================
   S (k + v + i) <= v

subgoal 2 (ID 10056) is:
 #(k + (v - 1)) = #(k + v - 1)
subgoal 3 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 4 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

trivial.

3 subgoals, subgoal 1 (ID 10056)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  l1 : j + i <= v - 1
  l2 : j < k + v
  ============================
   #(k + (v - 1)) = #(k + v - 1)

subgoal 2 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

destruct v.

4 subgoals, subgoal 1 (ID 10180)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < 0
  l0 : S (j + i) <= 0
  l1 : j + i <= 0 - 1
  l2 : j < k + 0
  ============================
   #(k + (0 - 1)) = #(k + 0 - 1)

subgoal 2 (ID 10186) is:
 #(k + (S v - 1)) = #(k + S v - 1)
subgoal 3 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 4 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

apply lt_n_O in l; elim l.

3 subgoals, subgoal 1 (ID 10186)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  l1 : j + i <= S v - 1
  l2 : j < k + S v
  ============================
   #(k + (S v - 1)) = #(k + S v - 1)

subgoal 2 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

rewrite <- 2! pred_of_minus.

3 subgoals, subgoal 1 (ID 10190)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  l1 : j + i <= S v - 1
  l2 : j < k + S v
  ============================
   #(k + pred (S v)) = #(pred (k + S v))

subgoal 2 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

replace (k+ S v) with (S (k+v)) by intuition.

3 subgoals, subgoal 1 (ID 10194)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  l1 : j + i <= S v - 1
  l2 : j < k + S v
  ============================
   #(k + pred (S v)) = #(pred (S (k + v)))

subgoal 2 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

simpl.

3 subgoals, subgoal 1 (ID 10209)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  l1 : j + i <= S v - 1
  l2 : j < k + S v
  ============================
   #(k + v) = #(k + v)

subgoal 2 (ID 10040) is:
 #(v - 1) =
 match lt_eq_lt_dec (k + v) j with
 | inleft (left _) => #(k + v)
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(k + v - 1)
 end
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 10040)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  g : j + i > v - 1
  ============================
   #(v - 1) =
   match lt_eq_lt_dec (k + v) j with
   | inleft (left _) => #(k + v)
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(k + v - 1)
   end

subgoal 2 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

elim (lt_irrefl v).

2 subgoals, subgoal 1 (ID 10210)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  g : j + i > v - 1
  ============================
   v < v

subgoal 2 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

apply lt_le_trans with (S (j+i)).

3 subgoals, subgoal 1 (ID 10211)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  g : j + i > v - 1
  ============================
   v < S (j + i)

subgoal 2 (ID 10212) is:
 S (j + i) <= v
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

destruct v.

4 subgoals, subgoal 1 (ID 10221)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < 0
  l0 : S (j + i) <= 0
  g : j + i > 0 - 1
  ============================
   0 < S (j + i)

subgoal 2 (ID 10226) is:
 S v < S (j + i)
subgoal 3 (ID 10212) is:
 S (j + i) <= v
subgoal 4 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

apply lt_n_O in l; elim l.

3 subgoals, subgoal 1 (ID 10226)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  g : j + i > S v - 1
  ============================
   S v < S (j + i)

subgoal 2 (ID 10212) is:
 S (j + i) <= v
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

rewrite <- pred_of_minus in g.

3 subgoals, subgoal 1 (ID 10230)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  g : j + i > pred (S v)
  ============================
   S v < S (j + i)

subgoal 2 (ID 10212) is:
 S (j + i) <= v
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

simpl in g.

3 subgoals, subgoal 1 (ID 10231)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  l0 : S (j + i) <= S v
  g : j + i > v
  ============================
   S v < S (j + i)

subgoal 2 (ID 10212) is:
 S (j + i) <= v
subgoal 3 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

intuition.

2 subgoals, subgoal 1 (ID 10212)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  l0 : S (j + i) <= v
  g : j + i > v - 1
  ============================
   S (j + i) <= v

subgoal 2 (ID 10029) is:
 #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]
(dependent evars:)

trivial.

1 subgoals, subgoal 1 (ID 10029)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  ============================
   #(v - 1) ↑  k # (j + i) = #v [j ←  N ↑  k # i]

(dependent evars:)

simpl.

1 subgoals, subgoal 1 (ID 10244)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  ============================
   (if le_gt_dec (j + i) (v - 1) then #(k + (v - 1)) else #(v - 1)) =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

(dependent evars:)

destruct (le_gt_dec (j+i) (v-1)).

2 subgoals, subgoal 1 (ID 10253)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  ============================
   #(k + (v - 1)) =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

destruct (lt_eq_lt_dec v j) as [[] | ].

4 subgoals, subgoal 1 (ID 10268)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  l1 : v < j
  ============================
   #(k + (v - 1)) = #v

subgoal 2 (ID 10269) is:
 #(k + (v - 1)) = N ↑  k # i ↑  j
subgoal 3 (ID 10270) is:
 #(k + (v - 1)) = #(v - 1)
subgoal 4 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

elim (lt_irrefl j); apply lt_trans with v; trivial.

3 subgoals, subgoal 1 (ID 10269)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  e : v = j
  ============================
   #(k + (v - 1)) = N ↑  k # i ↑  j

subgoal 2 (ID 10270) is:
 #(k + (v - 1)) = #(v - 1)
subgoal 3 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

subst.

3 subgoals, subgoal 1 (ID 10280)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < j
  g : S (j + i) > j
  l0 : j + i <= j - 1
  ============================
   #(k + (j - 1)) = N ↑  k # i ↑  j

subgoal 2 (ID 10270) is:
 #(k + (v - 1)) = #(v - 1)
subgoal 3 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

elim (lt_irrefl j); trivial.

2 subgoals, subgoal 1 (ID 10270)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  l1 : j < v
  ============================
   #(k + (v - 1)) = #(v - 1)

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

elim (lt_irrefl v).

2 subgoals, subgoal 1 (ID 10282)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  l1 : j < v
  ============================
   v < v

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

apply lt_le_trans with (S (j+i)).

3 subgoals, subgoal 1 (ID 10283)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  l1 : j < v
  ============================
   v < S (j + i)

subgoal 2 (ID 10284) is:
 S (j + i) <= v
subgoal 3 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

intuition.

2 subgoals, subgoal 1 (ID 10284)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  l0 : j + i <= v - 1
  l1 : j < v
  ============================
   S (j + i) <= v

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

destruct v.

3 subgoals, subgoal 1 (ID 10294)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < 0
  g : S (j + i) > 0
  l0 : j + i <= 0 - 1
  l1 : j < 0
  ============================
   S (j + i) <= 0

subgoal 2 (ID 10300) is:
 S (j + i) <= S v
subgoal 3 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

apply lt_n_O in l; elim l.

2 subgoals, subgoal 1 (ID 10300)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  g : S (j + i) > S v
  l0 : j + i <= S v - 1
  l1 : j < S v
  ============================
   S (j + i) <= S v

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

rewrite <- pred_of_minus in l0.

2 subgoals, subgoal 1 (ID 10304)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  g : S (j + i) > S v
  l0 : j + i <= pred (S v)
  l1 : j < S v
  ============================
   S (j + i) <= S v

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

simpl in l0.

2 subgoals, subgoal 1 (ID 10305)
  
  v : nat
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < S v
  g : S (j + i) > S v
  l0 : j + i <= v
  l1 : j < S v
  ============================
   S (j + i) <= S v

subgoal 2 (ID 10254) is:
 #(v - 1) =
 match lt_eq_lt_dec v j with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  k # i ↑  j
 | inright _ => #(v - 1)
 end
(dependent evars:)

intuition.

1 subgoals, subgoal 1 (ID 10254)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  g0 : j + i > v - 1
  ============================
   #(v - 1) =
   match lt_eq_lt_dec v j with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k # i ↑  j
   | inright _ => #(v - 1)
   end

(dependent evars:)

destruct (lt_eq_lt_dec) as [[] | ].

3 subgoals, subgoal 1 (ID 10331)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  g0 : j + i > v - 1
  l0 : v < j
  ============================
   #(v - 1) = #v

subgoal 2 (ID 10332) is:
 #(v - 1) = N ↑  k # i ↑  j
subgoal 3 (ID 10333) is:
 #(v - 1) = #(v - 1)
(dependent evars:)

elim (lt_irrefl j); apply lt_trans with v; trivial.

2 subgoals, subgoal 1 (ID 10332)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  g0 : j + i > v - 1
  e : v = j
  ============================
   #(v - 1) = N ↑  k # i ↑  j

subgoal 2 (ID 10333) is:
 #(v - 1) = #(v - 1)
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 10343)
  
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < j
  g : S (j + i) > j
  g0 : j + i > j - 1
  ============================
   #(j - 1) = N ↑  k # i ↑  j

subgoal 2 (ID 10333) is:
 #(v - 1) = #(v - 1)
(dependent evars:)

elim (lt_irrefl j); trivial.

1 subgoals, subgoal 1 (ID 10333)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  k : nat
  l : j < v
  g : S (j + i) > v
  g0 : j + i > v - 1
  l0 : j < v
  ============================
   #(v - 1) = #(v - 1)

(dependent evars:)

trivial.

No more subgoals.
(dependent evars:)

Qed.

substP1 is defined

Lemma substP2: (forall M N i j n, i <= n -> (M ↑ j # i ) [ j +n ← N ] = ( M [ n ← N ]) ↑ j # i )/\
(forall H N i j n, i <= n -> (H ↑h j # i ) [ j +n ←h N ] = ( H [ n ←h N ]) ↑h j # i ).

1 subgoals, subgoal 1 (ID 10357)
  
  ============================
   (forall (M N : Term) (i j n : nat),
    i <= n -> M ↑  j # i [(j + n) ←  N] = M [n ←  N] ↑  j # i) /\
   (forall (H : Prf) (N : Term) (i j n : nat),
    i <= n -> H ↑h j # i [(j + n) ←h N] = H [n ←h N] ↑h j # i)

(dependent evars:)

apply Term_induc;intros;simpl;
try rewrite H; intuition; try rewrite H0; intuition;
try rewrite <- (H0 N (S i) j (S n)); try rewrite <- (H1 N (S i) j (S n)); intuition;
replace (S(j+n)) with (j+(S n)) by intuition;try reflexivity.

1 subgoals, subgoal 1 (ID 10862)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  ============================
   (if le_gt_dec i v then #(j + v) else #v) [(j + n) ←  N] =
   match lt_eq_lt_dec v n with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  n
   | inright _ => #(v - 1)
   end ↑  j # i

(dependent evars:)

try replace (S(S(j+i))) with (S((S j)+i)) by intuition;
try rewrite H; intuition; try rewrite H0; intuition; try rewrite H1; intuition;
try rewrite <- (H0 N i (S j) k );try rewrite <- (H1 N i (S j) k);intuition.

1 subgoals, subgoal 1 (ID 10967)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  ============================
   (if le_gt_dec i v then #(j + v) else #v) [(j + n) ←  N] =
   match lt_eq_lt_dec v n with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  n
   | inright _ => #(v - 1)
   end ↑  j # i

(dependent evars:)

destruct (le_gt_dec i v); destruct (lt_eq_lt_dec v n) as [[] | ].

6 subgoals, subgoal 1 (ID 11036)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  ============================
   #(j + v) [(j + n) ←  N] = #v ↑  j # i

subgoal 2 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

simpl.

6 subgoals, subgoal 1 (ID 11055)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = (if le_gt_dec i v then #(j + v) else #v)

subgoal 2 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (le_gt_dec i v).

7 subgoals, subgoal 1 (ID 11064)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  l1 : i <= v
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(j + v)

subgoal 2 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 3 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 5 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 6 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 7 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (lt_eq_lt_dec (j+v) (j+n)) as [[] | ].

9 subgoals, subgoal 1 (ID 11079)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  l1 : i <= v
  l2 : j + v < j + n
  ============================
   #(j + v) = #(j + v)

subgoal 2 (ID 11080) is:
 N ↑  (j + n) = #(j + v)
subgoal 3 (ID 11081) is:
 #(j + v - 1) = #(j + v)
subgoal 4 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 5 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 7 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 8 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 9 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

reflexivity.

8 subgoals, subgoal 1 (ID 11080)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  l1 : i <= v
  e : j + v = j + n
  ============================
   N ↑  (j + n) = #(j + v)

subgoal 2 (ID 11081) is:
 #(j + v - 1) = #(j + v)
subgoal 3 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 4 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 6 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 7 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 8 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply plus_reg_l in e.

8 subgoals, subgoal 1 (ID 11084)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  l1 : i <= v
  e : v = n
  ============================
   N ↑  (j + n) = #(j + v)

subgoal 2 (ID 11081) is:
 #(j + v - 1) = #(j + v)
subgoal 3 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 4 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 6 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 7 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 8 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

subst.

8 subgoals, subgoal 1 (ID 11091)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  l0 : n < n
  l1 : i <= n
  ============================
   N ↑  (j + n) = #(j + n)

subgoal 2 (ID 11081) is:
 #(j + v - 1) = #(j + v)
subgoal 3 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 4 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 6 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 7 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 8 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl n); trivial.

7 subgoals, subgoal 1 (ID 11081)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  l1 : i <= v
  l2 : j + n < j + v
  ============================
   #(j + v - 1) = #(j + v)

subgoal 2 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 3 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 5 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 6 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 7 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply plus_lt_reg_l in l2.

7 subgoals, subgoal 1 (ID 11094)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  l1 : i <= v
  l2 : n < v
  ============================
   #(j + v - 1) = #(j + v)

subgoal 2 (ID 11065) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #v
subgoal 3 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 5 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 6 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 7 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_asym v n); trivial.

6 subgoals, subgoal 1 (ID 11065)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  g : i > v
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #v

subgoal 2 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl i).

6 subgoals, subgoal 1 (ID 11097)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : v < n
  g : i > v
  ============================
   i < i

subgoal 2 (ID 11037) is:
 #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply le_lt_trans with v; intuition.

5 subgoals, subgoal 1 (ID 11037)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  e : v = n
  ============================
   #(j + v) [(j + n) ←  N] = N ↑  n ↑  j # i

subgoal 2 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

subst.

5 subgoals, subgoal 1 (ID 11104)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  ============================
   #(j + n) [(j + n) ←  N] = N ↑  n ↑  j # i

subgoal 2 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

simpl.

5 subgoals, subgoal 1 (ID 11105)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  ============================
   match lt_eq_lt_dec (j + n) (j + n) with
   | inleft (left _) => #(j + n)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + n - 1)
   end = N ↑  n ↑  j # i

subgoal 2 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (lt_eq_lt_dec (j+n) (j+n)) as [[] | ].

7 subgoals, subgoal 1 (ID 11119)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  l0 : j + n < j + n
  ============================
   #(j + n) = N ↑  n ↑  j # i

subgoal 2 (ID 11120) is:
 N ↑  (j + n) = N ↑  n ↑  j # i
subgoal 3 (ID 11121) is:
 #(j + n - 1) = N ↑  n ↑  j # i
subgoal 4 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 5 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 6 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 7 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply lt_irrefl in l0; elim l0.

6 subgoals, subgoal 1 (ID 11120)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  e : j + n = j + n
  ============================
   N ↑  (j + n) = N ↑  n ↑  j # i

subgoal 2 (ID 11121) is:
 #(j + n - 1) = N ↑  n ↑  j # i
subgoal 3 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

symmetry.

6 subgoals, subgoal 1 (ID 11125)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  e : j + n = j + n
  ============================
   N ↑  n ↑  j # i = N ↑  (j + n)

subgoal 2 (ID 11121) is:
 #(j + n - 1) = N ↑  n ↑  j # i
subgoal 3 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply liftP3; intuition.

5 subgoals, subgoal 1 (ID 11121)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  l0 : j + n < j + n
  ============================
   #(j + n - 1) = N ↑  n ↑  j # i

subgoal 2 (ID 11038) is:
 #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply lt_irrefl in l0; elim l0.

4 subgoals, subgoal 1 (ID 11038)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  ============================
   #(j + v) [(j + n) ←  N] = #(v - 1) ↑  j # i

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

simpl.

4 subgoals, subgoal 1 (ID 11144)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = (if le_gt_dec i (v - 1) then #(j + (v - 1)) else #(v - 1))

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (le_gt_dec i (v-1)).

5 subgoals, subgoal 1 (ID 11153)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  l1 : i <= v - 1
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(j + (v - 1))

subgoal 2 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (lt_eq_lt_dec (j+v) (j+n))as [[] | ].

7 subgoals, subgoal 1 (ID 11168)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  l1 : i <= v - 1
  l2 : j + v < j + n
  ============================
   #(j + v) = #(j + (v - 1))

subgoal 2 (ID 11169) is:
 N ↑  (j + n) = #(j + (v - 1))
subgoal 3 (ID 11170) is:
 #(j + v - 1) = #(j + (v - 1))
subgoal 4 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 5 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 6 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 7 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply plus_lt_reg_l in l2.

7 subgoals, subgoal 1 (ID 11172)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  l1 : i <= v - 1
  l2 : v < n
  ============================
   #(j + v) = #(j + (v - 1))

subgoal 2 (ID 11169) is:
 N ↑  (j + n) = #(j + (v - 1))
subgoal 3 (ID 11170) is:
 #(j + v - 1) = #(j + (v - 1))
subgoal 4 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 5 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 6 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 7 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_asym v n ); trivial.

6 subgoals, subgoal 1 (ID 11169)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  l1 : i <= v - 1
  e : j + v = j + n
  ============================
   N ↑  (j + n) = #(j + (v - 1))

subgoal 2 (ID 11170) is:
 #(j + v - 1) = #(j + (v - 1))
subgoal 3 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply plus_reg_l in e; subst.

6 subgoals, subgoal 1 (ID 11183)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= n
  l0 : n < n
  l1 : i <= n - 1
  ============================
   N ↑  (j + n) = #(j + (n - 1))

subgoal 2 (ID 11170) is:
 #(j + v - 1) = #(j + (v - 1))
subgoal 3 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl n); trivial.

5 subgoals, subgoal 1 (ID 11170)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  l1 : i <= v - 1
  l2 : j + n < j + v
  ============================
   #(j + v - 1) = #(j + (v - 1))

subgoal 2 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct v.

6 subgoals, subgoal 1 (ID 11194)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= 0
  l0 : n < 0
  l1 : i <= 0 - 1
  l2 : j + n < j + 0
  ============================
   #(j + 0 - 1) = #(j + (0 - 1))

subgoal 2 (ID 11200) is:
 #(j + S v - 1) = #(j + (S v - 1))
subgoal 3 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 4 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 5 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 6 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply lt_n_O in l0; elim l0.

5 subgoals, subgoal 1 (ID 11200)
  
  v : nat
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= S v
  l0 : n < S v
  l1 : i <= S v - 1
  l2 : j + n < j + S v
  ============================
   #(j + S v - 1) = #(j + (S v - 1))

subgoal 2 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

rewrite <- 2! pred_of_minus.

5 subgoals, subgoal 1 (ID 11204)
  
  v : nat
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= S v
  l0 : n < S v
  l1 : i <= S v - 1
  l2 : j + n < j + S v
  ============================
   #(pred (j + S v)) = #(j + pred (S v))

subgoal 2 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

replace (j+ S v) with (S (j+v)) by intuition.

5 subgoals, subgoal 1 (ID 11208)
  
  v : nat
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= S v
  l0 : n < S v
  l1 : i <= S v - 1
  l2 : j + n < j + S v
  ============================
   #(pred (S (j + v))) = #(j + pred (S v))

subgoal 2 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

simpl.

5 subgoals, subgoal 1 (ID 11224)
  
  v : nat
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= S v
  l0 : n < S v
  l1 : i <= S v - 1
  l2 : j + n < j + S v
  ============================
   #(j + v) = #(j + v)

subgoal 2 (ID 11154) is:
 match lt_eq_lt_dec (j + v) (j + n) with
 | inleft (left _) => #(j + v)
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(j + v - 1)
 end = #(v - 1)
subgoal 3 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

trivial.

4 subgoals, subgoal 1 (ID 11154)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : i > v - 1
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(v - 1)

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

unfold gt in g.

4 subgoals, subgoal 1 (ID 11225)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : v - 1 < i
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(v - 1)

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

unfold lt in g.

4 subgoals, subgoal 1 (ID 11226)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : S (v - 1) <= i
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(v - 1)

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

rewrite <- pred_of_minus in g.

4 subgoals, subgoal 1 (ID 11228)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : S (pred v) <= i
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(v - 1)

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

rewrite <- (S_pred v n l0) in g.

4 subgoals, subgoal 1 (ID 11230)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : v <= i
  ============================
   match lt_eq_lt_dec (j + v) (j + n) with
   | inleft (left _) => #(j + v)
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(j + v - 1)
   end = #(v - 1)

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl n).

4 subgoals, subgoal 1 (ID 11231)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : v <= i
  ============================
   n < n

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply lt_le_trans with v; trivial.

4 subgoals, subgoal 1 (ID 11233)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  l : i <= v
  l0 : n < v
  g : v <= i
  ============================
   v <= n

subgoal 2 (ID 11052) is:
 #v [(j + n) ←  N] = #v ↑  j # i
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply le_trans with i; trivial.

3 subgoals, subgoal 1 (ID 11052)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  ============================
   #v [(j + n) ←  N] = #v ↑  j # i

subgoal 2 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

simpl.

3 subgoals, subgoal 1 (ID 11236)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  ============================
   match lt_eq_lt_dec v (j + n) with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(v - 1)
   end = (if le_gt_dec i v then #(j + v) else #v)

subgoal 2 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (le_gt_dec i v).

4 subgoals, subgoal 1 (ID 11245)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  l0 : i <= v
  ============================
   match lt_eq_lt_dec v (j + n) with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(v - 1)
   end = #(j + v)

subgoal 2 (ID 11246) is:
 match lt_eq_lt_dec v (j + n) with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(v - 1)
 end = #v
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl i).

4 subgoals, subgoal 1 (ID 11247)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  l0 : i <= v
  ============================
   i < i

subgoal 2 (ID 11246) is:
 match lt_eq_lt_dec v (j + n) with
 | inleft (left _) => #v
 | inleft (right _) => N ↑  (j + n)
 | inright _ => #(v - 1)
 end = #v
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply le_lt_trans with v; trivial.

3 subgoals, subgoal 1 (ID 11246)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  ============================
   match lt_eq_lt_dec v (j + n) with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(v - 1)
   end = #v

subgoal 2 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

destruct (lt_eq_lt_dec v (j+n)) as [[] | ].

5 subgoals, subgoal 1 (ID 11263)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  l0 : v < j + n
  ============================
   #v = #v

subgoal 2 (ID 11264) is:
 N ↑  (j + n) = #v
subgoal 3 (ID 11265) is:
 #(v - 1) = #v
subgoal 4 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 5 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

reflexivity.

4 subgoals, subgoal 1 (ID 11264)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  e : v = j + n
  ============================
   N ↑  (j + n) = #v

subgoal 2 (ID 11265) is:
 #(v - 1) = #v
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

subst.

4 subgoals, subgoal 1 (ID 11273)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > j + n
  l : j + n < n
  g0 : i > j + n
  ============================
   N ↑  (j + n) = #(j + n)

subgoal 2 (ID 11265) is:
 #(v - 1) = #v
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl n).

4 subgoals, subgoal 1 (ID 11274)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > j + n
  l : j + n < n
  g0 : i > j + n
  ============================
   n < n

subgoal 2 (ID 11265) is:
 #(v - 1) = #v
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply le_lt_trans with (j+n); intuition.

3 subgoals, subgoal 1 (ID 11265)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  l0 : j + n < v
  ============================
   #(v - 1) = #v

subgoal 2 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl n).

3 subgoals, subgoal 1 (ID 11286)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  l0 : j + n < v
  ============================
   n < n

subgoal 2 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply lt_trans with v.

4 subgoals, subgoal 1 (ID 11287)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  l0 : j + n < v
  ============================
   n < v

subgoal 2 (ID 11288) is:
 v < n
subgoal 3 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 4 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply le_lt_trans with (j+n); intuition.

3 subgoals, subgoal 1 (ID 11288)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : v < n
  g0 : i > v
  l0 : j + n < v
  ============================
   v < n

subgoal 2 (ID 11053) is:
 #v [(j + n) ←  N] = N ↑  n ↑  j # i
subgoal 3 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 11053)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  e : v = n
  ============================
   #v [(j + n) ←  N] = N ↑  n ↑  j # i

subgoal 2 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

simpl.

2 subgoals, subgoal 1 (ID 11302)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  e : v = n
  ============================
   match lt_eq_lt_dec v (j + n) with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(v - 1)
   end = N ↑  n ↑  j # i

subgoal 2 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 11307)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > n
  ============================
   match lt_eq_lt_dec n (j + n) with
   | inleft (left _) => #n
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(n - 1)
   end = N ↑  n ↑  j # i

subgoal 2 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

elim (lt_irrefl n).

2 subgoals, subgoal 1 (ID 11308)
  
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > n
  ============================
   n < n

subgoal 2 (ID 11054) is:
 #v [(j + n) ←  N] = #(v - 1) ↑  j # i
(dependent evars:)

apply lt_le_trans with i; intuition.

1 subgoals, subgoal 1 (ID 11054)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : n < v
  ============================
   #v [(j + n) ←  N] = #(v - 1) ↑  j # i

(dependent evars:)

simpl.

1 subgoals, subgoal 1 (ID 11311)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : n < v
  ============================
   match lt_eq_lt_dec v (j + n) with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  (j + n)
   | inright _ => #(v - 1)
   end = (if le_gt_dec i (v - 1) then #(j + (v - 1)) else #(v - 1))

(dependent evars:)

elim (lt_irrefl n).

1 subgoals, subgoal 1 (ID 11312)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : n < v
  ============================
   n < n

(dependent evars:)

apply lt_le_trans with v; intuition.

1 subgoals, subgoal 1 (ID 11314)
  
  v : Vars
  N : Term
  i : nat
  j : nat
  n : nat
  H : i <= n
  g : i > v
  l : n < v
  ============================
   v <= n

(dependent evars:)

apply le_trans with i; intuition.

No more subgoals.
(dependent evars:)

Qed.

substP2 is defined

Lemma substP3: (forall M N i k n, i <= k -> k <= i +n -> (M ↑ (S n ) # i ) [ k ← N ] = M ↑ n # i )/\
(forall H N i k n, i <= k -> k <= i +n -> (H ↑h (S n ) # i ) [ k ←h N ] = H ↑h n # i ).

1 subgoals, subgoal 1 (ID 11359)
  
  ============================
   (forall (M N : Term) (i k n : nat),
    i <= k -> k <= i + n -> M ↑  (S n) # i [k ←  N] = M ↑  n # i) /\
   (forall (H : Prf) (N : Term) (i k n : nat),
    i <= k -> k <= i + n -> H ↑h (S n) # i [k ←h N] = H ↑h n # i)

(dependent evars:)

apply Term_induc;intros;simpl;
try rewrite H; intuition; try rewrite H0; intuition; try rewrite H1; intuition;
replace (S i + n) with (S (i+n));intuition.

1 subgoals, subgoal 1 (ID 13502)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  ============================
   (if le_gt_dec i v then #(S (n + v)) else #v) [k ←  N] =
   (if le_gt_dec i v then #(n + v) else #v)

(dependent evars:)

destruct (le_gt_dec i v).

2 subgoals, subgoal 1 (ID 13604)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  ============================
   #(S (n + v)) [k ←  N] = #(n + v)

subgoal 2 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

unfold subst_rec.

2 subgoals, subgoal 1 (ID 13606)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  ============================
   match lt_eq_lt_dec (S (n + v)) k with
   | inleft (left _) => #(S (n + v))
   | inleft (right _) => N ↑  k
   | inright _ => #(S (n + v) - 1)
   end = #(n + v)

subgoal 2 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

destruct (lt_eq_lt_dec (S(n+v)) k) as [[] | ].

4 subgoals, subgoal 1 (ID 13620)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : S (n + v) < k
  ============================
   #(S (n + v)) = #(n + v)

subgoal 2 (ID 13621) is:
 N ↑  k = #(n + v)
subgoal 3 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 4 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

elim (lt_irrefl (i+n)).

4 subgoals, subgoal 1 (ID 13623)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : S (n + v) < k
  ============================
   i + n < i + n

subgoal 2 (ID 13621) is:
 N ↑  k = #(n + v)
subgoal 3 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 4 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

apply lt_le_trans with k; intuition.

4 subgoals, subgoal 1 (ID 13624)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : S (n + v) < k
  ============================
   i + n < k

subgoal 2 (ID 13621) is:
 N ↑  k = #(n + v)
subgoal 3 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 4 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

apply le_lt_trans with (v+n).

5 subgoals, subgoal 1 (ID 13682)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : S (n + v) < k
  ============================
   i + n <= v + n

subgoal 2 (ID 13683) is:
 v + n < k
subgoal 3 (ID 13621) is:
 N ↑  k = #(n + v)
subgoal 4 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 5 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

intuition.

4 subgoals, subgoal 1 (ID 13683)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : S (n + v) < k
  ============================
   v + n < k

subgoal 2 (ID 13621) is:
 N ↑  k = #(n + v)
subgoal 3 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 4 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

rewrite plus_comm; intuition.

3 subgoals, subgoal 1 (ID 13621)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  e : S (n + v) = k
  ============================
   N ↑  k = #(n + v)

subgoal 2 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 3 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

subst.

3 subgoals, subgoal 1 (ID 13731)
  
  v : Vars
  N : Term
  i : nat
  n : nat
  l : i <= v
  H : i <= S (n + v)
  H0 : S (n + v) <= i + n
  ============================
   N ↑  (S (n + v)) = #(n + v)

subgoal 2 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 3 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

replace (i+n) with (n+i) in H0 by (apply plus_comm) .

3 subgoals, subgoal 1 (ID 13736)
  
  v : Vars
  N : Term
  i : nat
  n : nat
  l : i <= v
  H : i <= S (n + v)
  H0 : S (n + v) <= n + i
  ============================
   N ↑  (S (n + v)) = #(n + v)

subgoal 2 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 3 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

replace (S (n+v)) with (n + S v) in H0 by intuition.

3 subgoals, subgoal 1 (ID 13742)
  
  v : Vars
  N : Term
  i : nat
  n : nat
  l : i <= v
  H : i <= S (n + v)
  H0 : n + S v <= n + i
  ============================
   N ↑  (S (n + v)) = #(n + v)

subgoal 2 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 3 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

apply plus_le_reg_l in H0.

3 subgoals, subgoal 1 (ID 13758)
  
  v : Vars
  N : Term
  i : nat
  n : nat
  l : i <= v
  H : i <= S (n + v)
  H0 : S v <= i
  ============================
   N ↑  (S (n + v)) = #(n + v)

subgoal 2 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 3 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

elim (lt_irrefl i).

3 subgoals, subgoal 1 (ID 13759)
  
  v : Vars
  N : Term
  i : nat
  n : nat
  l : i <= v
  H : i <= S (n + v)
  H0 : S v <= i
  ============================
   i < i

subgoal 2 (ID 13622) is:
 #(S (n + v) - 1) = #(n + v)
subgoal 3 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

apply le_lt_trans with v; intuition.

2 subgoals, subgoal 1 (ID 13622)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : k < S (n + v)
  ============================
   #(S (n + v) - 1) = #(n + v)

subgoal 2 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

simpl.

2 subgoals, subgoal 1 (ID 13762)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : k < S (n + v)
  ============================
   #(n + v - 0) = #(n + v)

subgoal 2 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

rewrite <- minus_n_O.

2 subgoals, subgoal 1 (ID 13763)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  l : i <= v
  l0 : k < S (n + v)
  ============================
   #(n + v) = #(n + v)

subgoal 2 (ID 13605) is:
 #v [k ←  N] = #v
(dependent evars:)

trivial.

1 subgoals, subgoal 1 (ID 13605)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  ============================
   #v [k ←  N] = #v

(dependent evars:)

simpl.

1 subgoals, subgoal 1 (ID 13764)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  ============================
   match lt_eq_lt_dec v k with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  k
   | inright _ => #(v - 1)
   end = #v

(dependent evars:)

destruct (lt_eq_lt_dec v k) as [[] | ].

3 subgoals, subgoal 1 (ID 13778)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : v < k
  ============================
   #v = #v

subgoal 2 (ID 13779) is:
 N ↑  k = #v
subgoal 3 (ID 13780) is:
 #(v - 1) = #v
(dependent evars:)

reflexivity.

2 subgoals, subgoal 1 (ID 13779)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  e : v = k
  ============================
   N ↑  k = #v

subgoal 2 (ID 13780) is:
 #(v - 1) = #v
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 13786)
  
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > k
  ============================
   N ↑  k = #k

subgoal 2 (ID 13780) is:
 #(v - 1) = #v
(dependent evars:)

elim (lt_irrefl i).

2 subgoals, subgoal 1 (ID 13787)
  
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > k
  ============================
   i < i

subgoal 2 (ID 13780) is:
 #(v - 1) = #v
(dependent evars:)

apply le_lt_trans with k; intuition.

1 subgoals, subgoal 1 (ID 13780)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : k < v
  ============================
   #(v - 1) = #v

(dependent evars:)

elim (lt_irrefl k).

1 subgoals, subgoal 1 (ID 13790)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : k < v
  ============================
   k < k

(dependent evars:)

apply lt_trans with v; trivial.

1 subgoals, subgoal 1 (ID 13792)
  
  v : Vars
  N : Term
  i : nat
  k : nat
  n : nat
  H : i <= k
  H0 : k <= i + n
  g : i > v
  l : k < v
  ============================
   v < k

(dependent evars:)

apply lt_le_trans with i; intuition.

No more subgoals.
(dependent evars:)

Qed.

substP3 is defined

Lemma substP4: (forall M N P i j, (M [ i ← N ]) [i +j ← P ] = (M [S(i +j) ← P ]) [i ← N [j ← P ]])/\
(forall H N P i j, (H [ i ←h N ]) [i +j ←h P ] = (H [S(i +j) ←h P ]) [i ←h N [j ← P ]]).

1 subgoals, subgoal 1 (ID 13807)
  
  ============================
   (forall (M N P : Term) (i j : nat),
    M [i ←  N] [(i + j) ←  P] = M [(S (i + j)) ←  P] [i ←  N [j ←  P]]) /\
   (forall (H : Prf) (N P : Term) (i j : nat),
    H [i ←h N] [(i + j) ←h P] = H [(S (i + j)) ←h P] [i ←h N [j ←  P]])

(dependent evars:)

apply Term_induc;intros;simpl;
[|(try rewrite H; intuition;replace (S(S(i+j))) with (S((S i)+ j)) by intuition;
try rewrite <- H0; intuition; replace (S(i+j)) with ((S i)+ j) by intuition;
try rewrite H1; intuition)..].

1 subgoals, subgoal 1 (ID 13924)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  ============================
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N ↑  i
   | inright _ => #(v - 1)
   end [(i + j) ←  P] =
   match lt_eq_lt_dec v (S (i + j)) with
   | inleft (left _) => #v
   | inleft (right _) => P ↑  (S (i + j))
   | inright _ => #(v - 1)
   end [i ←  N [j ←  P]]

(dependent evars:)

destruct (lt_eq_lt_dec v i) as [[] | ] ; destruct (lt_eq_lt_dec v (S(i+j))) as [[] | ].

9 subgoals, subgoal 1 (ID 14186)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  ============================
   #v [(i + j) ←  P] = #v [i ←  N [j ←  P]]

subgoal 2 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

simpl.

9 subgoals, subgoal 1 (ID 14221)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  ============================
   match lt_eq_lt_dec v (i + j) with
   | inleft (left _) => #v
   | inleft (right _) => P ↑  (i + j)
   | inright _ => #(v - 1)
   end =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

destruct (lt_eq_lt_dec v (i+j)) as [[] | ].

11 subgoals, subgoal 1 (ID 14235)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : v < i + j
  ============================
   #v =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14236) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 6 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 7 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 8 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 9 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 10 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 11 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

destruct (lt_eq_lt_dec v i) as [[] | ].

13 subgoals, subgoal 1 (ID 14251)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : v < i + j
  l2 : v < i
  ============================
   #v = #v

subgoal 2 (ID 14252) is:
 #v = N [j ←  P] ↑  i
subgoal 3 (ID 14253) is:
 #v = #(v - 1)
subgoal 4 (ID 14236) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 5 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 6 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 8 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 9 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 10 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 11 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 12 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 13 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

trivial.

12 subgoals, subgoal 1 (ID 14252)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : v < i + j
  e : v = i
  ============================
   #v = N [j ←  P] ↑  i

subgoal 2 (ID 14253) is:
 #v = #(v - 1)
subgoal 3 (ID 14236) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 5 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 10 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 11 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 12 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

12 subgoals, subgoal 1 (ID 14260)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < i
  l0 : i < S (i + j)
  l1 : i < i + j
  ============================
   #i = N [j ←  P] ↑  i

subgoal 2 (ID 14253) is:
 #v = #(v - 1)
subgoal 3 (ID 14236) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 5 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 10 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 11 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 12 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply lt_irrefl in l; elim l.

11 subgoals, subgoal 1 (ID 14253)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : v < i + j
  l2 : i < v
  ============================
   #v = #(v - 1)

subgoal 2 (ID 14236) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 6 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 7 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 8 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 9 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 10 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 11 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim ( lt_asym v i); trivial.

10 subgoals, subgoal 1 (ID 14236)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  e : v = i + j
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 8 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 9 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 10 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

10 subgoals, subgoal 1 (ID 14270)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i + j < i
  l0 : i + j < S (i + j)
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (i + j) i with
   | inleft (left _) => #(i + j)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(i + j - 1)
   end

subgoal 2 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 8 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 9 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 10 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite plus_comm in l.

10 subgoals, subgoal 1 (ID 14272)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : j + i < i
  l0 : i + j < S (i + j)
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (i + j) i with
   | inleft (left _) => #(i + j)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(i + j - 1)
   end

subgoal 2 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 8 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 9 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 10 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i).

10 subgoals, subgoal 1 (ID 14273)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : j + i < i
  l0 : i + j < S (i + j)
  ============================
   i < i

subgoal 2 (ID 14237) is:
 #(v - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 8 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 9 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 10 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

induction j; simpl in *; intuition.

9 subgoals, subgoal 1 (ID 14237)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : i + j < v
  ============================
   #(v - 1) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i).

9 subgoals, subgoal 1 (ID 14324)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : i + j < v
  ============================
   i < i

subgoal 2 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply le_lt_trans with v;intuition.

9 subgoals, subgoal 1 (ID 14325)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : i + j < v
  ============================
   i <= v

subgoal 2 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite plus_comm in l1; intuition.

9 subgoals, subgoal 1 (ID 14347)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : v < S (i + j)
  l1 : j + i < v
  ============================
   i <= v

subgoal 2 (ID 14187) is:
 #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 7 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 8 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 9 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

induction j; simpl in *; intuition.

8 subgoals, subgoal 1 (ID 14187)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  e : v = S (i + j)
  ============================
   #v [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 6 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 7 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 8 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

8 subgoals, subgoal 1 (ID 14443)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : S (i + j) < i
  ============================
   #(S (i + j)) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 6 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 7 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 8 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i).

8 subgoals, subgoal 1 (ID 14444)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : S (i + j) < i
  ============================
   i < i

subgoal 2 (ID 14188) is:
 #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 6 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 7 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 8 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply lt_trans with (S (i+j)); intuition.

7 subgoals, subgoal 1 (ID 14188)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : S (i + j) < v
  ============================
   #v [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]

subgoal 2 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 3 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i).

7 subgoals, subgoal 1 (ID 14489)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : S (i + j) < v
  ============================
   i < i

subgoal 2 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 3 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply lt_trans with (S (i+j)); intuition.

7 subgoals, subgoal 1 (ID 14491)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : v < i
  l0 : S (i + j) < v
  ============================
   S (i + j) < i

subgoal 2 (ID 14202) is:
 N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 3 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply lt_trans with v; trivial.

6 subgoals, subgoal 1 (ID 14202)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  e : v = i
  l : v < S (i + j)
  ============================
   N ↑  i [(i + j) ←  P] = #v [i ←  N [j ←  P]]

subgoal 2 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

simpl.

6 subgoals, subgoal 1 (ID 14592)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  e : v = i
  l : v < S (i + j)
  ============================
   N ↑  i [(i + j) ←  P] =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

6 subgoals, subgoal 1 (ID 14597)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  ============================
   N ↑  i [(i + j) ←  P] =
   match lt_eq_lt_dec i i with
   | inleft (left _) => #i
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(i - 1)
   end

subgoal 2 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

destruct (lt_eq_lt_dec i i) as [[] | ].

8 subgoals, subgoal 1 (ID 14611)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  l0 : i < i
  ============================
   N ↑  i [(i + j) ←  P] = #i

subgoal 2 (ID 14612) is:
 N ↑  i [(i + j) ←  P] = N [j ←  P] ↑  i
subgoal 3 (ID 14613) is:
 N ↑  i [(i + j) ←  P] = #(i - 1)
subgoal 4 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 6 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 7 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 8 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i); trivial.

7 subgoals, subgoal 1 (ID 14612)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  e : i = i
  ============================
   N ↑  i [(i + j) ←  P] = N [j ←  P] ↑  i

subgoal 2 (ID 14613) is:
 N ↑  i [(i + j) ←  P] = #(i - 1)
subgoal 3 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 5 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 6 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply substP2; intuition.

6 subgoals, subgoal 1 (ID 14613)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  l0 : i < i
  ============================
   N ↑  i [(i + j) ←  P] = #(i - 1)

subgoal 2 (ID 14203) is:
 N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 4 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 5 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i); trivial.

5 subgoals, subgoal 1 (ID 14203)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  e : v = i
  e0 : v = S (i + j)
  ============================
   N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

5 subgoals, subgoal 1 (ID 14633)
  
  N : Term
  P : Term
  i : nat
  j : nat
  e0 : i = S (i + j)
  ============================
   N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite plus_comm in e0.

5 subgoals, subgoal 1 (ID 14635)
  
  N : Term
  P : Term
  i : nat
  j : nat
  e0 : i = S (j + i)
  ============================
   N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply succ_plus_discr in e0.

5 subgoals, subgoal 1 (ID 14637)
  
  N : Term
  P : Term
  i : nat
  j : nat
  e0 : False
  ============================
   N ↑  i [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14204) is:
 N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
subgoal 3 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 4 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim e0.

4 subgoals, subgoal 1 (ID 14204)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  e : v = i
  l : S (i + j) < v
  ============================
   N ↑  i [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]

subgoal 2 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

4 subgoals, subgoal 1 (ID 14642)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : S (i + j) < i
  ============================
   N ↑  i [(i + j) ←  P] = #(i - 1) [i ←  N [j ←  P]]

subgoal 2 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i).

4 subgoals, subgoal 1 (ID 14643)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : S (i + j) < i
  ============================
   i < i

subgoal 2 (ID 14218) is:
 #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply le_lt_trans with (i+j); intuition.

3 subgoals, subgoal 1 (ID 14218)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  ============================
   #(v - 1) [(i + j) ←  P] = #v [i ←  N [j ←  P]]

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

simpl.

3 subgoals, subgoal 1 (ID 14671)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  ============================
   match lt_eq_lt_dec (v - 1) (i + j) with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => P ↑  (i + j)
   | inright _ => #(v - 1 - 1)
   end =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

destruct (lt_eq_lt_dec (v-1) (i+j)) as [[] | ].

5 subgoals, subgoal 1 (ID 14685)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : v - 1 < i + j
  ============================
   #(v - 1) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14686) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

destruct (lt_eq_lt_dec v i) as [[] | ].

7 subgoals, subgoal 1 (ID 14701)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : v - 1 < i + j
  l2 : v < i
  ============================
   #(v - 1) = #v

subgoal 2 (ID 14702) is:
 #(v - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14703) is:
 #(v - 1) = #(v - 1)
subgoal 4 (ID 14686) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 5 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 6 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 7 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_asym v i); trivial.

6 subgoals, subgoal 1 (ID 14702)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : v - 1 < i + j
  e : v = i
  ============================
   #(v - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14703) is:
 #(v - 1) = #(v - 1)
subgoal 3 (ID 14686) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 5 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

6 subgoals, subgoal 1 (ID 14712)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < i
  l0 : i < S (i + j)
  l1 : i - 1 < i + j
  ============================
   #(i - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14703) is:
 #(v - 1) = #(v - 1)
subgoal 3 (ID 14686) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 5 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 6 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl i); trivial.

5 subgoals, subgoal 1 (ID 14703)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : v - 1 < i + j
  l2 : i < v
  ============================
   #(v - 1) = #(v - 1)

subgoal 2 (ID 14686) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 4 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 5 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

trivial.

4 subgoals, subgoal 1 (ID 14686)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  e : v - 1 = i + j
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite <- e in l0.

4 subgoals, subgoal 1 (ID 14715)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (v - 1)
  e : v - 1 = i + j
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite <- pred_of_minus in l0.

4 subgoals, subgoal 1 (ID 14717)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (pred v)
  e : v - 1 = i + j
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite <- (S_pred v i l) in l0.

4 subgoals, subgoal 1 (ID 14719)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < v
  e : v - 1 = i + j
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14687) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec v i with
 | inleft (left _) => #v
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1)
 end
subgoal 3 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl v); trivial.

3 subgoals, subgoal 1 (ID 14687)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : i + j < v - 1
  ============================
   #(v - 1 - 1) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply lt_n_S in l1.

3 subgoals, subgoal 1 (ID 14722)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : S (i + j) < S (v - 1)
  ============================
   #(v - 1 - 1) =
   match lt_eq_lt_dec v i with
   | inleft (left _) => #v
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1)
   end

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl v).

3 subgoals, subgoal 1 (ID 14723)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : S (i + j) < S (v - 1)
  ============================
   v < v

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply lt_trans with (S(i+j)); trivial.

3 subgoals, subgoal 1 (ID 14725)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : S (i + j) < S (v - 1)
  ============================
   S (i + j) < v

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite <- pred_of_minus in l1.

3 subgoals, subgoal 1 (ID 14727)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : S (i + j) < S (pred v)
  ============================
   S (i + j) < v

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite <- (S_pred v i l) in l1.

3 subgoals, subgoal 1 (ID 14729)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : v < S (i + j)
  l1 : S (i + j) < v
  ============================
   S (i + j) < v

subgoal 2 (ID 14219) is:
 #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 14219)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  e : v = S (i + j)
  ============================
   #(v - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 14734)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  ============================
   #(S (i + j) - 1) [(i + j) ←  P] = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

simpl.

2 subgoals, subgoal 1 (ID 14735)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  ============================
   match lt_eq_lt_dec (i + j - 0) (i + j) with
   | inleft (left _) => #(i + j - 0)
   | inleft (right _) => P ↑  (i + j)
   | inright _ => #(i + j - 0 - 1)
   end = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

rewrite <- minus_n_O.

2 subgoals, subgoal 1 (ID 14736)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  ============================
   match lt_eq_lt_dec (i + j) (i + j) with
   | inleft (left _) => #(i + j)
   | inleft (right _) => P ↑  (i + j)
   | inright _ => #(i + j - 1)
   end = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

destruct (lt_eq_lt_dec (i+j) (i+j)) as [[] | ].

4 subgoals, subgoal 1 (ID 14750)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  l0 : i + j < i + j
  ============================
   #(i + j) = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14751) is:
 P ↑  (i + j) = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14752) is:
 #(i + j - 1) = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 4 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl (i+j)) ; trivial.

3 subgoals, subgoal 1 (ID 14751)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  e : i + j = i + j
  ============================
   P ↑  (i + j) = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14752) is:
 #(i + j - 1) = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

symmetry.

3 subgoals, subgoal 1 (ID 14755)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  e : i + j = i + j
  ============================
   P ↑  (S (i + j)) [i ←  N [j ←  P]] = P ↑  (i + j)

subgoal 2 (ID 14752) is:
 #(i + j - 1) = P ↑  (S (i + j)) [i ←  N [j ←  P]]
subgoal 3 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

apply substP3; intuition.

2 subgoals, subgoal 1 (ID 14752)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  l0 : i + j < i + j
  ============================
   #(i + j - 1) = P ↑  (S (i + j)) [i ←  N [j ←  P]]

subgoal 2 (ID 14220) is:
 #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]
(dependent evars:)

elim (lt_irrefl (i+j)) ; trivial.

1 subgoals, subgoal 1 (ID 14220)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  ============================
   #(v - 1) [(i + j) ←  P] = #(v - 1) [i ←  N [j ←  P]]

(dependent evars:)

simpl.

1 subgoals, subgoal 1 (ID 14780)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  ============================
   match lt_eq_lt_dec (v - 1) (i + j) with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => P ↑  (i + j)
   | inright _ => #(v - 1 - 1)
   end =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

(dependent evars:)

destruct (lt_eq_lt_dec (v-1) (i+j)) as [[] | ].

3 subgoals, subgoal 1 (ID 14794)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : v - 1 < i + j
  ============================
   #(v - 1) =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

subgoal 2 (ID 14795) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
subgoal 3 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

elim (lt_irrefl v).

3 subgoals, subgoal 1 (ID 14797)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : v - 1 < i + j
  ============================
   v < v

subgoal 2 (ID 14795) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
subgoal 3 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

apply lt_trans with (S (i+j)) ;trivial.

3 subgoals, subgoal 1 (ID 14798)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : v - 1 < i + j
  ============================
   v < S (i + j)

subgoal 2 (ID 14795) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
subgoal 3 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

apply lt_n_S in l1.

3 subgoals, subgoal 1 (ID 14801)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : S (v - 1) < S (i + j)
  ============================
   v < S (i + j)

subgoal 2 (ID 14795) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
subgoal 3 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

rewrite <- pred_of_minus in l1.

3 subgoals, subgoal 1 (ID 14803)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : S (pred v) < S (i + j)
  ============================
   v < S (i + j)

subgoal 2 (ID 14795) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
subgoal 3 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

rewrite <- (S_pred v i l) in l1.

3 subgoals, subgoal 1 (ID 14805)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : v < S (i + j)
  ============================
   v < S (i + j)

subgoal 2 (ID 14795) is:
 P ↑  (i + j) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
subgoal 3 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 14795)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  e : v - 1 = i + j
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

subgoal 2 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

apply eq_S in e.

2 subgoals, subgoal 1 (ID 14807)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  e : S (v - 1) = S (i + j)
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

subgoal 2 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

rewrite <- pred_of_minus in e.

2 subgoals, subgoal 1 (ID 14809)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  e : S (pred v) = S (i + j)
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

subgoal 2 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

rewrite <- (S_pred v i l) in e.

2 subgoals, subgoal 1 (ID 14811)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  e : v = S (i + j)
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

subgoal 2 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 14817)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S (i + j)
  l0 : S (i + j) < S (i + j)
  ============================
   P ↑  (i + j) =
   match lt_eq_lt_dec (S (i + j) - 1) i with
   | inleft (left _) => #(S (i + j) - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(S (i + j) - 1 - 1)
   end

subgoal 2 (ID 14796) is:
 #(v - 1 - 1) =
 match lt_eq_lt_dec (v - 1) i with
 | inleft (left _) => #(v - 1)
 | inleft (right _) => N [j ←  P] ↑  i
 | inright _ => #(v - 1 - 1)
 end
(dependent evars:)

elim (lt_irrefl (S(i+j))); trivial.

1 subgoals, subgoal 1 (ID 14796)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : i + j < v - 1
  ============================
   #(v - 1 - 1) =
   match lt_eq_lt_dec (v - 1) i with
   | inleft (left _) => #(v - 1)
   | inleft (right _) => N [j ←  P] ↑  i
   | inright _ => #(v - 1 - 1)
   end

(dependent evars:)

destruct (lt_eq_lt_dec (v-1) i) as [[] | ].

3 subgoals, subgoal 1 (ID 14832)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : i + j < v - 1
  l2 : v - 1 < i
  ============================
   #(v - 1 - 1) = #(v - 1)

subgoal 2 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

elim (lt_irrefl v).

3 subgoals, subgoal 1 (ID 14835)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : i + j < v - 1
  l2 : v - 1 < i
  ============================
   v < v

subgoal 2 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

apply le_lt_trans with i; trivial.

3 subgoals, subgoal 1 (ID 14836)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : i + j < v - 1
  l2 : v - 1 < i
  ============================
   v <= i

subgoal 2 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

destruct v.

4 subgoals, subgoal 1 (ID 14847)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < 0
  l0 : S (i + j) < 0
  l1 : i + j < 0 - 1
  l2 : 0 - 1 < i
  ============================
   0 <= i

subgoal 2 (ID 14853) is:
 S v <= i
subgoal 3 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 4 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

apply lt_n_O in l; elim l.

3 subgoals, subgoal 1 (ID 14853)
  
  v : nat
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S v
  l0 : S (i + j) < S v
  l1 : i + j < S v - 1
  l2 : S v - 1 < i
  ============================
   S v <= i

subgoal 2 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

rewrite <- pred_of_minus in l2.

3 subgoals, subgoal 1 (ID 14857)
  
  v : nat
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S v
  l0 : S (i + j) < S v
  l1 : i + j < S v - 1
  l2 : pred (S v) < i
  ============================
   S v <= i

subgoal 2 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

simpl in l2.

3 subgoals, subgoal 1 (ID 14858)
  
  v : nat
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S v
  l0 : S (i + j) < S v
  l1 : i + j < S v - 1
  l2 : v < i
  ============================
   S v <= i

subgoal 2 (ID 14833) is:
 #(v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 14833)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : i + j < v - 1
  e : v - 1 = i
  ============================
   #(v - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

destruct v.

3 subgoals, subgoal 1 (ID 14868)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < 0
  l0 : S (i + j) < 0
  l1 : i + j < 0 - 1
  e : 0 - 1 = i
  ============================
   #(0 - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14874) is:
 #(S v - 1 - 1) = N [j ←  P] ↑  i
subgoal 3 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

elim (lt_n_O i); trivial.

2 subgoals, subgoal 1 (ID 14874)
  
  v : nat
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S v
  l0 : S (i + j) < S v
  l1 : i + j < S v - 1
  e : S v - 1 = i
  ============================
   #(S v - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

rewrite <- pred_of_minus in e.

2 subgoals, subgoal 1 (ID 14877)
  
  v : nat
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S v
  l0 : S (i + j) < S v
  l1 : i + j < S v - 1
  e : pred (S v) = i
  ============================
   #(S v - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

simpl in e.

2 subgoals, subgoal 1 (ID 14878)
  
  v : nat
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S v
  l0 : S (i + j) < S v
  l1 : i + j < S v - 1
  e : v = i
  ============================
   #(S v - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

subst.

2 subgoals, subgoal 1 (ID 14885)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S i
  l0 : S (i + j) < S i
  l1 : i + j < S i - 1
  ============================
   #(S i - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

rewrite <- pred_of_minus in l1.

2 subgoals, subgoal 1 (ID 14887)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S i
  l0 : S (i + j) < S i
  l1 : i + j < pred (S i)
  ============================
   #(S i - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

simpl in l1.

2 subgoals, subgoal 1 (ID 14888)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S i
  l0 : S (i + j) < S i
  l1 : i + j < i
  ============================
   #(S i - 1 - 1) = N [j ←  P] ↑  i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

elim (lt_irrefl i).

2 subgoals, subgoal 1 (ID 14889)
  
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < S i
  l0 : S (i + j) < S i
  l1 : i + j < i
  ============================
   i < i

subgoal 2 (ID 14834) is:
 #(v - 1 - 1) = #(v - 1 - 1)
(dependent evars:)

apply le_lt_trans with (i+j); intuition.

1 subgoals, subgoal 1 (ID 14834)
  
  v : Vars
  N : Term
  P : Term
  i : nat
  j : nat
  l : i < v
  l0 : S (i + j) < v
  l1 : i + j < v - 1
  l2 : i < v - 1
  ============================
   #(v - 1 - 1) = #(v - 1 - 1)

(dependent evars:)

trivial.

No more subgoals.
(dependent evars:)

Qed.

substP4 is defined

Lemma subst_travers : (forall M N P n, (M [← N ]) [n ← P ] = (M [n +1 ← P ])[← N [n ← P ]])/\
(forall H N P n, (H [←h N ]) [n ←h P ] = (H [n +1 ←h P ])[←h N [n ← P ]]).

1 subgoals, subgoal 1 (ID 14910)
  
  ============================
   (forall (M N P : Term) (n : nat),
    M [ ← N] [n ←  P] = (M [(n + 1) ←  P]) [ ← N [n ←  P]]) /\
   (forall (H : Prf) (N P : Term) (n : nat),
    H [ ←h N] [n ←h P] = (H [(n + 1) ←h P]) [ ←h N [n ←  P]])

(dependent evars:)

destruct substP4;split;intros;simpl;rewrite plus_comm;
change (1+n) with (S n); change n with (0+n); intuition.

No more subgoals.
(dependent evars:)

Qed.

subst_travers is defined

The following two lemmas will be useful for the erasure operation defined later.

Lemma erasure_lem1 : (forall a n, a = (a ↑ 1 # (S n )) [n ← #0])/\
(forall H n, H = (H ↑h 1 # (S n )) [n ←h #0]).

1 subgoals, subgoal 1 (ID 14963)
  
  ============================
   (forall (a : Term) (n : nat), a = a ↑  1 # (S n) [n ←  #0]) /\
   (forall (H : Prf) (n : nat), H = H ↑h 1 # (S n) [n ←h #0])

(dependent evars:)

apply Term_induc;intros;
[unfold lift_rec;destruct le_gt_dec;unfold subst_rec;destruct lt_eq_lt_dec as [[]|];simpl;subst;
try rewrite <- minus_n_O;try rewrite <- plus_n_O;try trivial; elim (lt_irrefl v);simpl in *
|simpl;try rewrite <- H;try rewrite <- H0;try rewrite <- H1;trivial..].

3 subgoals, subgoal 1 (ID 15109)
  
  v : Vars
  n : nat
  l : S n <= v
  l0 : S v < n
  ============================
   v < v

subgoal 2 (ID 15112) is:
 v < v
subgoal 3 (ID 15117) is:
 v < v
(dependent evars:)

apply lt_trans with (S v);try apply lt_n_Sn; apply lt_trans with n;assumption.

2 subgoals, subgoal 1 (ID 15112)
  
  v : Vars
  l : S (S v) <= v
  ============================
   v < v

subgoal 2 (ID 15117) is:
 v < v
(dependent evars:)

apply lt_trans with (S v);try assumption;apply lt_n_Sn.

1 subgoals, subgoal 1 (ID 15117)
  
  v : Vars
  n : nat
  g : S n > v
  l : n < v
  ============================
   v < v

(dependent evars:)

apply le_lt_trans with n;try assumption; apply gt_S_le;exact g.

No more subgoals.
(dependent evars:)

Qed.

erasure_lem1 is defined

Lemma erasure_lem3 : (forall n m t, m >n->#m = (#m ↑ 1 # (S n )) [n ← t ]).

1 subgoals, subgoal 1 (ID 15166)
  
  ============================
   forall (n m : nat) (t : Term), m > n -> #m = #m ↑  1 # (S n) [n ←  t]

(dependent evars:)

intros.

1 subgoals, subgoal 1 (ID 15170)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  ============================
   #m = #m ↑  1 # (S n) [n ←  t]

(dependent evars:)

unfold lift_rec;destruct le_gt_dec.

2 subgoals, subgoal 1 (ID 15180)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  l : S n <= m
  ============================
   #m = #(1 + m) [n ←  t]

subgoal 2 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

unfold subst_rec;destruct lt_eq_lt_dec as [[]|];simpl in *.

4 subgoals, subgoal 1 (ID 15205)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  l : S n <= m
  l0 : S m < n
  ============================
   #m = #(S m)

subgoal 2 (ID 15212) is:
 #m = t ↑  n
subgoal 3 (ID 15219) is:
 #m = #(m - 0)
subgoal 4 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

destruct (lt_irrefl n).

4 subgoals, subgoal 1 (ID 15224)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  l : S n <= m
  l0 : S m < n
  ============================
   n < n

subgoal 2 (ID 15212) is:
 #m = t ↑  n
subgoal 3 (ID 15219) is:
 #m = #(m - 0)
subgoal 4 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

apply lt_trans with m;[assumption|apply lt_trans with (S m);[do 2 constructor|assumption]].

3 subgoals, subgoal 1 (ID 15212)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  l : S n <= m
  e : S m = n
  ============================
   #m = t ↑  n

subgoal 2 (ID 15219) is:
 #m = #(m - 0)
subgoal 3 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

subst.

3 subgoals, subgoal 1 (ID 15235)
  
  m : nat
  t : Term
  H : m > S m
  l : S (S m) <= m
  ============================
   #m = t ↑  (S m)

subgoal 2 (ID 15219) is:
 #m = #(m - 0)
subgoal 3 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

destruct (lt_irrefl m).

3 subgoals, subgoal 1 (ID 15240)
  
  m : nat
  t : Term
  H : m > S m
  l : S (S m) <= m
  ============================
   m < m

subgoal 2 (ID 15219) is:
 #m = #(m - 0)
subgoal 3 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

apply lt_trans with (S m);[do 2 constructor|assumption].

2 subgoals, subgoal 1 (ID 15219)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  l : S n <= m
  l0 : n < S m
  ============================
   #m = #(m - 0)

subgoal 2 (ID 15181) is:
 #m = #m [n ←  t]
(dependent evars:)

rewrite <- minus_n_O;reflexivity.

1 subgoals, subgoal 1 (ID 15181)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  g : S n > m
  ============================
   #m = #m [n ←  t]

(dependent evars:)

destruct (lt_irrefl n).

1 subgoals, subgoal 1 (ID 15250)
  
  n : nat
  m : nat
  t : Term
  H : m > n
  g : S n > m
  ============================
   n < n

(dependent evars:)

apply lt_le_trans with m;[|apply le_S_n];assumption.

No more subgoals.
(dependent evars:)

Qed.

erasure_lem3 is defined

Here some more lemmas about a lift or substitution being equal to a lifted term

Lemma lift_is_lift_sublemma : forall j v, j <v->exists w,#v =w ↑1#j.

1 subgoals, subgoal 1 (ID 15258)
  
  ============================
   forall j v : nat, j < v -> exists w : Term, #v = w ↑  1 # j

(dependent evars:)

intros.

1 subgoals, subgoal 1 (ID 15261)
  
  j : nat
  v : nat
  H : j < v
  ============================
   exists w : Term, #v = w ↑  1 # j

(dependent evars:)

exists #(v-1).

1 subgoals, subgoal 1 (ID 15263)
  
  j : nat
  v : nat
  H : j < v
  ============================
   #v = #(v - 1) ↑  1 # j

(dependent evars:)

assert (S(v-1)=v).

2 subgoals, subgoal 1 (ID 15265)
  
  j : nat
  v : nat
  H : j < v
  ============================
   S (v - 1) = v

subgoal 2 (ID 15266) is:
 #v = #(v - 1) ↑  1 # j
(dependent evars:)

rewrite (minus_Sn_m v 1);[simpl;rewrite <- (minus_n_O v);reflexivity|
unfold lt in H;apply le_trans with (S j);[apply le_n_S;apply le_0_n|assumption]].

1 subgoals, subgoal 1 (ID 15266)
  
  j : nat
  v : nat
  H : j < v
  H0 : S (v - 1) = v
  ============================
   #v = #(v - 1) ↑  1 # j

(dependent evars:)

simpl;destruct le_gt_dec.

2 subgoals, subgoal 1 (ID 15285)
  
  j : nat
  v : nat
  H : j < v
  H0 : S (v - 1) = v
  l : j <= v - 1
  ============================
   #v = #(S (v - 1))

subgoal 2 (ID 15286) is:
 #v = #(v - 1)
(dependent evars:)

rewrite H0;trivial.

1 subgoals, subgoal 1 (ID 15286)
  
  j : nat
  v : nat
  H : j < v
  H0 : S (v - 1) = v
  g : j > v - 1
  ============================
   #v = #(v - 1)

(dependent evars:)

destruct lt_irrefl with j;unfold gt in g;unfold lt in g.

1 subgoals, subgoal 1 (ID 15294)
  
  j : nat
  v : nat
  H : j < v
  H0 : S (v - 1) = v
  g : S (v - 1) <= j
  ============================
   j < j

(dependent evars:)

rewrite H0 in g.

1 subgoals, subgoal 1 (ID 15296)
  
  j : nat
  v : nat
  H : j < v
  H0 : S (v - 1) = v
  g : v <= j
  ============================
   j < j

(dependent evars:)

apply lt_le_trans with v;assumption.

No more subgoals.
(dependent evars:)

Qed.

lift_is_lift_sublemma is defined

Lemma lift_is_lift : (forall N A n i j,N ↑ i # n =A ↑ 1 # j -> j <n -> exists M,N =M ↑ 1 # j )/\
(forall N A n i j,N ↑h i # n =A ↑h 1 # j -> j <n -> exists M,N =M ↑h 1 # j ).

1 subgoals, subgoal 1 (ID 15315)
  
  ============================
   (forall (N A : Term) (n i j : nat),
    N ↑  i # n = A ↑  1 # j -> j < n -> exists M : Term, N = M ↑  1 # j) /\
   (forall (N A : Prf) (n i j : nat),
    N ↑h i # n = A ↑h 1 # j -> j < n -> exists M : Prf, N = M ↑h 1 # j)

(dependent evars:)

apply Term_induc;intros;
[|simpl in *;destruct A;simpl in *;try destruct le_gt_dec;try discriminate;
match goal with
| Heq : _ = _ |- _ => injection Heq;intros;clear Heq
end;
repeat match goal with
| IH : _ -> _ |- _ => edestruct IH;[eassumption|try apply lt_n_S;assumption|];clear IH
end;subst;
try match goal with
| |- exists _, ?f _ = _ => eexists (f _ );simpl;reflexivity
| |- exists _, ?f _ _ = _ => eexists (f _ _ );simpl;reflexivity
| |- exists _, ?f _ _ _ = _ => eexists (f _ _ _);simpl;reflexivity
end
..].

1 subgoals, subgoal 1 (ID 15336)
  
  v : Vars
  A : Term
  n : nat
  i : nat
  j : nat
  H : #v ↑  i # n = A ↑  1 # j
  H0 : j < n
  ============================
   exists M : Term, #v = M ↑  1 # j

(dependent evars: ?15637 using , ?15844 using , ?15845 using , ?15846 using , ?15847 using , ?15863 using , ?15864 using , ?15865 using , ?15866 using , ?15894 using , ?15895 using , ?16102 using , ?16103 using , ?16104 using , ?16105 using , ?16121 using , ?16122 using , ?16123 using , ?16124 using , ?16152 using , ?16153 using , ?16360 using , ?16361 using , ?16362 using , ?16363 using , ?16378 using , ?16379 using , ?16380 using , ?16381 using , ?16409 using , ?16410 using , ?16617 using , ?16618 using , ?16619 using , ?16620 using , ?16635 using , ?16636 using , ?16637 using , ?16638 using , ?16666 using , ?16667 using , ?16880 using , ?16881 using , ?16882 using , ?16883 using , ?16901 using , ?17114 using , ?17115 using , ?17116 using , ?17117 using , ?17135 using , ?17371 using , ?17372 using , ?17373 using , ?17374 using , ?17389 using , ?17390 using , ?17391 using , ?17392 using , ?17420 using , ?17421 using , ?17634 using , ?17635 using , ?17636 using , ?17637 using , ?17655 using , ?17914 using , ?17915 using , ?17916 using , ?17917 using , ?17933 using , ?17934 using , ?17935 using , ?17936 using , ?17951 using , ?17952 using , ?17953 using , ?17954 using , ?17993 using , ?17994 using , ?17995 using , ?18254 using , ?18255 using , ?18256 using , ?18257 using , ?18273 using , ?18274 using , ?18275 using , ?18276 using , ?18291 using , ?18292 using , ?18293 using , ?18294 using , ?18333 using , ?18334 using , ?18335 using , ?18571 using , ?18572 using , ?18573 using , ?18574 using , ?18589 using , ?18590 using , ?18591 using , ?18592 using , ?18620 using , ?18621 using , ?18834 using , ?18835 using , ?18836 using , ?18837 using , ?18855 using ,)

simpl in *;destruct le_gt_dec.

2 subgoals, subgoal 1 (ID 18885)
  
  v : Vars
  A : Term
  n : nat
  i : nat
  j : nat
  l : n <= v
  H : #(i + v) = A ↑  1 # j
  H0 : j < n
  ============================
   exists M : Term, #v = M ↑  1 # j

subgoal 2 (ID 18889) is:
 exists M : Term, #v = M ↑  1 # j
(dependent evars: ?15637 using , ?15844 using , ?15845 using , ?15846 using , ?15847 using , ?15863 using , ?15864 using , ?15865 using , ?15866 using , ?15894 using , ?15895 using , ?16102 using , ?16103 using , ?16104 using , ?16105 using , ?16121 using , ?16122 using , ?16123 using , ?16124 using , ?16152 using , ?16153 using , ?16360 using , ?16361 using , ?16362 using , ?16363 using , ?16378 using , ?16379 using , ?16380 using , ?16381 using , ?16409 using , ?16410 using , ?16617 using , ?16618 using , ?16619 using , ?16620 using , ?16635 using , ?16636 using , ?16637 using , ?16638 using , ?16666 using , ?16667 using , ?16880 using , ?16881 using , ?16882 using , ?16883 using , ?16901 using , ?17114 using , ?17115 using , ?17116 using , ?17117 using , ?17135 using , ?17371 using , ?17372 using , ?17373 using , ?17374 using , ?17389 using , ?17390 using , ?17391 using , ?17392 using , ?17420 using , ?17421 using , ?17634 using , ?17635 using , ?17636 using , ?17637 using , ?17655 using , ?17914 using , ?17915 using , ?17916 using , ?17917 using , ?17933 using , ?17934 using , ?17935 using , ?17936 using , ?17951 using , ?17952 using , ?17953 using , ?17954 using , ?17993 using , ?17994 using , ?17995 using , ?18254 using , ?18255 using , ?18256 using , ?18257 using , ?18273 using , ?18274 using , ?18275 using , ?18276 using , ?18291 using , ?18292 using , ?18293 using , ?18294 using , ?18333 using , ?18334 using , ?18335 using , ?18571 using , ?18572 using , ?18573 using , ?18574 using , ?18589 using , ?18590 using , ?18591 using , ?18592 using , ?18620 using , ?18621 using , ?18834 using , ?18835 using , ?18836 using , ?18837 using , ?18855 using ,)

apply lift_is_lift_sublemma.

2 subgoals, subgoal 1 (ID 18890)
  
  v : Vars
  A : Term
  n : nat
  i : nat
  j : nat
  l : n <= v
  H : #(i + v) = A ↑  1 # j
  H0 : j < n
  ============================
   j < v

subgoal 2 (ID 18889) is:
 exists M : Term, #v = M ↑  1 # j
(dependent evars: ?15637 using , ?15844 using , ?15845 using , ?15846 using , ?15847 using , ?15863 using , ?15864 using , ?15865 using , ?15866 using , ?15894 using , ?15895 using , ?16102 using , ?16103 using , ?16104 using , ?16105 using , ?16121 using , ?16122 using , ?16123 using , ?16124 using , ?16152 using , ?16153 using , ?16360 using , ?16361 using , ?16362 using , ?16363 using , ?16378 using , ?16379 using , ?16380 using , ?16381 using , ?16409 using , ?16410 using , ?16617 using , ?16618 using , ?16619 using , ?16620 using , ?16635 using , ?16636 using , ?16637 using , ?16638 using , ?16666 using , ?16667 using , ?16880 using , ?16881 using , ?16882 using , ?16883 using , ?16901 using , ?17114 using , ?17115 using , ?17116 using , ?17117 using , ?17135 using , ?17371 using , ?17372 using , ?17373 using , ?17374 using , ?17389 using , ?17390 using , ?17391 using , ?17392 using , ?17420 using , ?17421 using , ?17634 using , ?17635 using , ?17636 using , ?17637 using , ?17655 using , ?17914 using , ?17915 using , ?17916 using , ?17917 using , ?17933 using , ?17934 using , ?17935 using , ?17936 using , ?17951 using , ?17952 using , ?17953 using , ?17954 using , ?17993 using , ?17994 using , ?17995 using , ?18254 using , ?18255 using , ?18256 using , ?18257 using , ?18273 using , ?18274 using , ?18275 using , ?18276 using , ?18291 using , ?18292 using , ?18293 using , ?18294 using , ?18333 using , ?18334 using , ?18335 using , ?18571 using , ?18572 using , ?18573 using , ?18574 using , ?18589 using , ?18590 using , ?18591 using , ?18592 using , ?18620 using , ?18621 using , ?18834 using , ?18835 using , ?18836 using , ?18837 using , ?18855 using ,)

apply lt_le_trans with n;assumption.

1 subgoals, subgoal 1 (ID 18889)
  
  v : Vars
  A : Term
  n : nat
  i : nat
  j : nat
  g : n > v
  H : #v = A ↑  1 # j
  H0 : j < n
  ============================
   exists M : Term, #v = M ↑  1 # j

(dependent evars: ?15637 using , ?15844 using , ?15845 using , ?15846 using , ?15847 using , ?15863 using , ?15864 using , ?15865 using , ?15866 using , ?15894 using , ?15895 using , ?16102 using , ?16103 using , ?16104 using , ?16105 using , ?16121 using , ?16122 using , ?16123 using , ?16124 using , ?16152 using , ?16153 using , ?16360 using , ?16361 using , ?16362 using , ?16363 using , ?16378 using , ?16379 using , ?16380 using , ?16381 using , ?16409 using , ?16410 using , ?16617 using , ?16618 using , ?16619 using , ?16620 using , ?16635 using , ?16636 using , ?16637 using , ?16638 using , ?16666 using , ?16667 using , ?16880 using , ?16881 using , ?16882 using , ?16883 using , ?16901 using , ?17114 using , ?17115 using , ?17116 using , ?17117 using , ?17135 using , ?17371 using , ?17372 using , ?17373 using , ?17374 using , ?17389 using , ?17390 using , ?17391 using , ?17392 using , ?17420 using , ?17421 using , ?17634 using , ?17635 using , ?17636 using , ?17637 using , ?17655 using , ?17914 using , ?17915 using , ?17916 using , ?17917 using , ?17933 using , ?17934 using , ?17935 using , ?17936 using , ?17951 using , ?17952 using , ?17953 using , ?17954 using , ?17993 using , ?17994 using , ?17995 using , ?18254 using , ?18255 using , ?18256 using , ?18257 using , ?18273 using , ?18274 using , ?18275 using , ?18276 using , ?18291 using , ?18292 using , ?18293 using , ?18294 using , ?18333 using , ?18334 using , ?18335 using , ?18571 using , ?18572 using , ?18573 using , ?18574 using , ?18589 using , ?18590 using , ?18591 using , ?18592 using , ?18620 using , ?18621 using , ?18834 using , ?18835 using , ?18836 using , ?18837 using , ?18855 using ,)

econstructor;eassumption.

No more subgoals.
(dependent evars: ?15637 using , ?15844 using , ?15845 using , ?15846 using , ?15847 using , ?15863 using , ?15864 using , ?15865 using , ?15866 using , ?15894 using , ?15895 using , ?16102 using , ?16103 using , ?16104 using , ?16105 using , ?16121 using , ?16122 using , ?16123 using , ?16124 using , ?16152 using , ?16153 using , ?16360 using , ?16361 using , ?16362 using , ?16363 using , ?16378 using , ?16379 using , ?16380 using , ?16381 using , ?16409 using , ?16410 using , ?16617 using , ?16618 using , ?16619 using , ?16620 using , ?16635 using , ?16636 using , ?16637 using , ?16638 using , ?16666 using , ?16667 using , ?16880 using , ?16881 using , ?16882 using , ?16883 using , ?16901 using , ?17114 using , ?17115 using , ?17116 using , ?17117 using , ?17135 using , ?17371 using , ?17372 using , ?17373 using , ?17374 using , ?17389 using , ?17390 using , ?17391 using , ?17392 using , ?17420 using , ?17421 using , ?17634 using , ?17635 using , ?17636 using , ?17637 using , ?17655 using , ?17914 using , ?17915 using , ?17916 using , ?17917 using , ?17933 using , ?17934 using , ?17935 using , ?17936 using , ?17951 using , ?17952 using , ?17953 using , ?17954 using , ?17993 using , ?17994 using , ?17995 using , ?18254 using , ?18255 using , ?18256 using , ?18257 using , ?18273 using , ?18274 using , ?18275 using , ?18276 using , ?18291 using , ?18292 using , ?18293 using , ?18294 using , ?18333 using , ?18334 using , ?18335 using , ?18571 using , ?18572 using , ?18573 using , ?18574 using , ?18589 using , ?18590 using , ?18591 using , ?18592 using , ?18620 using , ?18621 using , ?18834 using , ?18835 using , ?18836 using , ?18837 using , ?18855 using , ?18894 using ,)

Qed.

lift_is_lift is defined

Lemma subst_is_lift : (forall N T A n j, N [n ← T ]=A ↑ 1#j->j <n->exists M,N =M ↑ 1#j )/\
(forall N T A n j, N [n ←h T ]=A ↑h1 #j->j <n->exists M,N =M ↑h1 #j ).

1 subgoals, subgoal 1 (ID 18912)
  
  ============================
   (forall (N T A : Term) (n j : nat),
    N [n ←  T] = A ↑  1 # j -> j < n -> exists M : Term, N = M ↑  1 # j) /\
   (forall (N : Prf) (T : Term) (A : Prf) (n j : nat),
    N [n ←h T] = A ↑h 1 # j -> j < n -> exists M : Prf, N = M ↑h 1 # j)

(dependent evars:)

1 subgoals, subgoal 1 (ID 18933)
  
  v : Vars
  T : Term
  A : Term
  n : nat
  j : nat
  H : #v [n ←  T] = A ↑  1 # j
  H0 : j < n
  ============================
   exists M : Term, #v = M ↑  1 # j

(dependent evars: ?19234 using , ?19441 using , ?19442 using , ?19443 using , ?19444 using , ?19460 using , ?19461 using , ?19462 using , ?19463 using , ?19491 using , ?19492 using , ?19699 using , ?19700 using , ?19701 using , ?19702 using , ?19718 using , ?19719 using , ?19720 using , ?19721 using , ?19749 using , ?19750 using , ?19957 using , ?19958 using , ?19959 using , ?19960 using , ?19975 using , ?19976 using , ?19977 using , ?19978 using , ?20006 using , ?20007 using , ?20214 using , ?20215 using , ?20216 using , ?20217 using , ?20232 using , ?20233 using , ?20234 using , ?20235 using , ?20263 using , ?20264 using , ?20477 using , ?20478 using , ?20479 using , ?20480 using , ?20498 using , ?20711 using , ?20712 using , ?20713 using , ?20714 using , ?20732 using , ?20968 using , ?20969 using , ?20970 using , ?20971 using , ?20986 using , ?20987 using , ?20988 using , ?20989 using , ?21017 using , ?21018 using , ?21231 using , ?21232 using , ?21233 using , ?21234 using , ?21252 using , ?21511 using , ?21512 using , ?21513 using , ?21514 using , ?21530 using , ?21531 using , ?21532 using , ?21533 using , ?21548 using , ?21549 using , ?21550 using , ?21551 using , ?21590 using , ?21591 using , ?21592 using , ?21851 using , ?21852 using , ?21853 using , ?21854 using , ?21870 using , ?21871 using , ?21872 using , ?21873 using , ?21888 using , ?21889 using , ?21890 using , ?21891 using , ?21930 using , ?21931 using , ?21932 using , ?22168 using , ?22169 using , ?22170 using , ?22171 using , ?22186 using , ?22187 using , ?22188 using , ?22189 using , ?22217 using , ?22218 using , ?22431 using , ?22432 using , ?22433 using , ?22434 using , ?22452 using ,)

unfold subst_rec in H;destruct lt_eq_lt_dec as [[]|];[exists A;assumption|apply lift_is_lift_sublemma..].

2 subgoals, subgoal 1 (ID 22491)
  
  v : Vars
  T : Term
  A : Term
  n : nat
  j : nat
  e : v = n
  H : T ↑  n = A ↑  1 # j
  H0 : j < n
  ============================
   j < v

subgoal 2 (ID 22492) is:
 j < v
(dependent evars: ?19234 using , ?19441 using , ?19442 using , ?19443 using , ?19444 using , ?19460 using , ?19461 using , ?19462 using , ?19463 using , ?19491 using , ?19492 using , ?19699 using , ?19700 using , ?19701 using , ?19702 using , ?19718 using , ?19719 using , ?19720 using , ?19721 using , ?19749 using , ?19750 using , ?19957 using , ?19958 using , ?19959 using , ?19960 using , ?19975 using , ?19976 using , ?19977 using , ?19978 using , ?20006 using , ?20007 using , ?20214 using , ?20215 using , ?20216 using , ?20217 using , ?20232 using , ?20233 using , ?20234 using , ?20235 using , ?20263 using , ?20264 using , ?20477 using , ?20478 using , ?20479 using , ?20480 using , ?20498 using , ?20711 using , ?20712 using , ?20713 using , ?20714 using , ?20732 using , ?20968 using , ?20969 using , ?20970 using , ?20971 using , ?20986 using , ?20987 using , ?20988 using , ?20989 using , ?21017 using , ?21018 using , ?21231 using , ?21232 using , ?21233 using , ?21234 using , ?21252 using , ?21511 using , ?21512 using , ?21513 using , ?21514 using , ?21530 using , ?21531 using , ?21532 using , ?21533 using , ?21548 using , ?21549 using , ?21550 using , ?21551 using , ?21590 using , ?21591 using , ?21592 using , ?21851 using , ?21852 using , ?21853 using , ?21854 using , ?21870 using , ?21871 using , ?21872 using , ?21873 using , ?21888 using , ?21889 using , ?21890 using , ?21891 using , ?21930 using , ?21931 using , ?21932 using , ?22168 using , ?22169 using , ?22170 using , ?22171 using , ?22186 using , ?22187 using , ?22188 using , ?22189 using , ?22217 using , ?22218 using , ?22431 using , ?22432 using , ?22433 using , ?22434 using , ?22452 using ,)

subst;assumption.

1 subgoals, subgoal 1 (ID 22492)
  
  v : Vars
  T : Term
  A : Term
  n : nat
  j : nat
  l : n < v
  H : #(v - 1) = A ↑  1 # j
  H0 : j < n
  ============================
   j < v

(dependent evars: ?19234 using , ?19441 using , ?19442 using , ?19443 using , ?19444 using , ?19460 using , ?19461 using , ?19462 using , ?19463 using , ?19491 using , ?19492 using , ?19699 using , ?19700 using , ?19701 using , ?19702 using , ?19718 using , ?19719 using , ?19720 using , ?19721 using , ?19749 using , ?19750 using , ?19957 using , ?19958 using , ?19959 using , ?19960 using , ?19975 using , ?19976 using , ?19977 using , ?19978 using , ?20006 using , ?20007 using , ?20214 using , ?20215 using , ?20216 using , ?20217 using , ?20232 using , ?20233 using , ?20234 using , ?20235 using , ?20263 using , ?20264 using , ?20477 using , ?20478 using , ?20479 using , ?20480 using , ?20498 using , ?20711 using , ?20712 using , ?20713 using , ?20714 using , ?20732 using , ?20968 using , ?20969 using , ?20970 using , ?20971 using , ?20986 using , ?20987 using , ?20988 using , ?20989 using , ?21017 using , ?21018 using , ?21231 using , ?21232 using , ?21233 using , ?21234 using , ?21252 using , ?21511 using , ?21512 using , ?21513 using , ?21514 using , ?21530 using , ?21531 using , ?21532 using , ?21533 using , ?21548 using , ?21549 using , ?21550 using , ?21551 using , ?21590 using , ?21591 using , ?21592 using , ?21851 using , ?21852 using , ?21853 using , ?21854 using , ?21870 using , ?21871 using , ?21872 using , ?21873 using , ?21888 using , ?21889 using , ?21890 using , ?21891 using , ?21930 using , ?21931 using , ?21932 using , ?22168 using , ?22169 using , ?22170 using , ?22171 using , ?22186 using , ?22187 using , ?22188 using , ?22189 using , ?22217 using , ?22218 using , ?22431 using , ?22432 using , ?22433 using , ?22434 using , ?22452 using ,)

apply lt_trans with n;assumption.

No more subgoals.
(dependent evars: ?19234 using , ?19441 using , ?19442 using , ?19443 using , ?19444 using , ?19460 using , ?19461 using , ?19462 using , ?19463 using , ?19491 using , ?19492 using , ?19699 using , ?19700 using , ?19701 using , ?19702 using , ?19718 using , ?19719 using , ?19720 using , ?19721 using , ?19749 using , ?19750 using , ?19957 using , ?19958 using , ?19959 using , ?19960 using , ?19975 using , ?19976 using , ?19977 using , ?19978 using , ?20006 using , ?20007 using , ?20214 using , ?20215 using , ?20216 using , ?20217 using , ?20232 using , ?20233 using , ?20234 using , ?20235 using , ?20263 using , ?20264 using , ?20477 using , ?20478 using , ?20479 using , ?20480 using , ?20498 using , ?20711 using , ?20712 using , ?20713 using , ?20714 using , ?20732 using , ?20968 using , ?20969 using , ?20970 using , ?20971 using , ?20986 using , ?20987 using , ?20988 using , ?20989 using , ?21017 using , ?21018 using , ?21231 using , ?21232 using , ?21233 using , ?21234 using , ?21252 using , ?21511 using , ?21512 using , ?21513 using , ?21514 using , ?21530 using , ?21531 using , ?21532 using , ?21533 using , ?21548 using , ?21549 using , ?21550 using , ?21551 using , ?21590 using , ?21591 using , ?21592 using , ?21851 using , ?21852 using , ?21853 using , ?21854 using , ?21870 using , ?21871 using , ?21872 using , ?21873 using , ?21888 using , ?21889 using , ?21890 using , ?21891 using , ?21930 using , ?21931 using , ?21932 using , ?22168 using , ?22169 using , ?22170 using , ?22171 using , ?22186 using , ?22187 using , ?22188 using , ?22189 using , ?22217 using , ?22218 using , ?22431 using , ?22432 using , ?22433 using , ?22434 using , ?22452 using ,)

Qed.

subst_is_lift is defined

End f_term_mod.

Module Type f_term_mod is defined

Index

This page has been generated by coqdoc