Require Import List.
Require Import Arith.
Require Import Omega.

Require Import MatchCompNat.

Require Syntax.
Module SetProgram(My_Program: Syntax.Program).
Import My_Program.

Require Semantics.
Module My_Semantics := Semantics.SetProgram(My_Program).
Import My_Semantics.

Import My_WellFormedness.
Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.

Lemma Successive_variable_liftings:
  forall (n1 n2 m: nat) (X: TypeVar) (k: nat),
    (lift_at_depth_in_typeVar (lift_at_depth_in_typeVar X (n1 + n2) k) m (k + n2)) =
    (lift_at_depth_in_typeVar X (n1 + n2 + m) k)
.

Lemma Successive_type_liftings_aux:
  forall (n1 n2 m: nat) (t: TypeS) (k: nat),
    (lift_at_depth_in_type (lift_at_depth_in_type t (n1 + n2) k) m (k + n2)) =
    (lift_at_depth_in_type t (n1 + n2 + m) k)
.
















Lemma Successive_type_liftings_cor1:
  forall (n m k: nat) (t : TypeS),
    n > k ->
    (lift_at_depth_in_type (lift_in_type t n) m k) =
    (lift_in_type t (n + m))
.

Lemma Successive_type_liftings:
  forall (t: TypeS) (n m: nat),
    (lift_in_type (lift_in_type t n) m) =
    (lift_in_type t (n + m))
.


Lemma Lifting_then_dropping_in_typeVar:
  forall (X: nat) (n k: nat),
    (drop_at_depth_in_typeVar (lift_at_depth_in_typeVar X (S n) k) k) =
    (lift_at_depth_in_typeVar X n k)
.






Lemma Lifting_then_dropping:
  forall (t: TypeS) (n k: nat),
    (drop_at_depth_in_type (lift_at_depth_in_type t (S n) k) k) =
    (lift_at_depth_in_type t n k)
.















Lemma lift_in_typeVar_by_zero:
  forall (i k: nat),
    (lift_at_depth_in_typeVar i 0 k) = i
.




Lemma lift_in_type_by_zero:
  forall (t: TypeS) (k: nat),
    (lift_at_depth_in_type t 0 k) = t
.














End SetProgram.