Require Import List.
Require Import Arith.

Require Import Util.
Require Import MatchCompNat.

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

Require Binders_proofs.
Module My_Binders_proofs := Binders_proofs.SetProgram(My_Program).
Import My_Binders_proofs.

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

Lemma Permuting_type_lifting_and_substitution_aux:
  forall (R: TypeS) (k1 n: nat) (t: TypeS) (k2: nat),
    (lift_at_depth_in_type (typeSubst_in_type t (k1 + k2) R) n k2) =
    (typeSubst_in_type (lift_at_depth_in_type t n k2) (k1 + k2 + n) R)
.


































Lemma Permuting_type_lifting_and_substitution:
  forall (t: TypeS) (X: TypeVar) (R: TypeS) (n: nat),
    (lift_in_type (typeSubst_in_type t X R) n) =
    (typeSubst_in_type (lift_in_type t n) (X + n) R)
.

Lemma Permuting_type_lifting_and_substitution_cor1:
  forall (t : TypeS) (X : TypeVar) (R : TypeS),
    (lift_in_type (typeSubst_in_type t X R) 1) =
    (typeSubst_in_type (lift_in_type t 1) (S X) R)
.



Lemma Permuting_type_liftings_aux:
  forall (k1 n1 n2: nat) (t: TypeS) (k2: nat),
    (lift_at_depth_in_type (lift_at_depth_in_type t n2 k2) n1 (k1 + n2 + k2)) =
    (lift_at_depth_in_type (lift_at_depth_in_type t n1 (k1 + k2)) n2 k2)
.


























Lemma Permuting_type_liftings_cor1:
  forall (k1 n1 n2: nat) (t: TypeS),
    (n2 <= k1) ->
    (lift_at_depth_in_type (lift_in_type t n2) n1 k1) =
    (lift_in_type (lift_at_depth_in_type t n1 (k1 - n2)) n2)
.

Lemma Permuting_type_lifting_and_substitution_2_aux:
  forall (R: TypeS) (k1 n: nat) (t: TypeS) (k2: nat),
    (lift_at_depth_in_type (typeSubst_in_type t k2 R) n (k1 + k2)) =
    (typeSubst_in_type (lift_at_depth_in_type t n (S (k1 + k2))) k2
      (lift_at_depth_in_type R n k1))
.





































Lemma Permuting_type_lifting_and_substitution_2_cor1:
  forall (R : TypeS) (k n : nat) (t : TypeS),
    (lift_at_depth_in_type (typeSubst_in_type t 0 R) n k) =
    (typeSubst_in_type (lift_at_depth_in_type t n (S k)) 0
                       (lift_at_depth_in_type R n k))
.



Lemma Type_lifting_stronger_than_substitution_aux:
  forall (n d: nat) (R t: TypeS) (k: nat),
    (typeSubst_in_type (lift_at_depth_in_type t (S (n + d)) k) (n + k) R) =
    (lift_at_depth_in_type t (n + d) k)
.
























Lemma Type_lifting_stronger_than_substitution:
  forall (n d: nat) (R t: TypeS),
    (typeSubst_in_type (lift_in_type t (S (n + d))) n R) =
    (lift_in_type t (n + d))
.

Lemma Permuting_type_substitutions:
  forall (R R': TypeS) (k: nat) (t: TypeS) (n: nat),
    (typeSubst_in_type (typeSubst_in_type t n R) (n + k) R') =
    (typeSubst_in_type (typeSubst_in_type t (S (n + k)) R') n (typeSubst_in_type R k R'))
.






































Lemma Permuting_type_substitutions_cor1:
  forall (R R': TypeS) (k: nat) (t: TypeS),
    (typeSubst_in_type (typeSubst_in_type t 0 R) k R') =
    (typeSubst_in_type (typeSubst_in_type t (S k) R') 0 (typeSubst_in_type R k R'))
.


Lemma Permuting_type_substitutions_cor2:
  forall (R R': TypeS) (k: nat) (t: TypeS),
    (typeSubst_in_type (typeSubst_in_type t 1 R) (S k) R') =
    (typeSubst_in_type (typeSubst_in_type t (S (S k)) R') 1 (typeSubst_in_type R k R'))
.


End SetProgram.