Require Import List.

Require Import Util.

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

Require BoundCompliantSubstitutions_proofs.
Module My_BoundCompliantSubstitutions_proofs := BoundCompliantSubstitutions_proofs.SetProgram(My_Program).
Import My_BoundCompliantSubstitutions_proofs.

Import My_Progress_proofs.
Import My_TransitivityElimination_proofs.
Import My_Normalization_proofs.
Import My_Subtyping_proofs.
Import My_Typing_proofs.
Import My_Confluence.
Import My_Auxiliary_proofs.
Import My_Substitutions_proofs.
Import My_Binders_proofs.
Import My_Semantics.
Import My_WellFormedness.
Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.


Definition typeSubst_in_termInfo (info: TermInfo) (k: nat) (R: TypeS): TermInfo :=
  match info with
    | (TermI T) => (TermI (typeSubst_in_type T k R))
    | (TermListI Ts) => (TermListI (map (fun T => (typeSubst_in_type T k R)) Ts))
    | (FieldTermListI N) => (FieldTermListI (typeSubst_in_type N k R))
  end
.


Definition TermEnv_WK (D: TypeEnv) (G: TermEnv): Prop :=
  List_forall (fun T => (Type_WK D T Type_)) G
.


Lemma Type_substitution_preserves_fields_of_fieldTermList:
  forall (fts: Term) (k: nat) (R: TypeS),
    (fields_of_fieldTermList (typeSubst_in_term fts k R)) =
    (fields_of_fieldTermList fts)
.











Lemma Permuting_type_substitutions_in_lists:
  forall (R R' : TypeS) (k : nat) (ts : (list TypeS)) (n : nat),
    (typeSubst_in_typeList (typeSubst_in_typeList ts n R) (n + k) R') =
    (typeSubst_in_typeList (typeSubst_in_typeList ts (S (n + k)) R')
                           n (typeSubst_in_type R k R'))
.




Lemma Permuting_type_substitutions_in_lists_cor1:
  forall (R R' : TypeS) (k : nat) (ts : (list TypeS)),
    (typeSubst_in_typeList (typeSubst_in_typeList ts 0 R) k R') =
    (typeSubst_in_typeList (typeSubst_in_typeList ts (S k) R')
                           0 (typeSubst_in_type R k R'))
.




Lemma Permuting_type_substitutions_in_lists_cor2:
  forall (R R' : TypeS) (k : nat) (ts : (list TypeS)),
    (typeSubst_in_typeList (typeSubst_in_typeList ts 1 R) (S k) R') =
    (typeSubst_in_typeList (typeSubst_in_typeList ts (S (S k)) R')
                           1 (typeSubst_in_type R k R'))
.





Theorem Type_substitution_preserves_typing:
  forall (D1 D2: TypeEnv) (G: TermEnv) (Pi R: TypeS) (k: KindS) (t: Term) (info: TermInfo),
    (Type_WK D1 R (TypeTuple k)) ->
    (SectionSat D1 R Pi) ->
    (TypeEnv_WK (D1 ++ (Pi :: D2))) ->
    (TermEnv_WK (D1 ++ (Pi :: D2)) G) ->
    (Term_WT (D1 ++ (Pi :: D2)) G t info) ->
    (Term_WT (D1 ++ (typeSubst_in_typeEnv D2 0 R))
             (map (fun T => (typeSubst_in_type T (length D2) R)) G)
             (typeSubst_in_term t (length D2) R)
             (typeSubst_in_termInfo info (length D2) R))
.





















































































Definition typeSubst_in_termEnv (G: TermEnv) (k: nat) (R: TypeS): TermEnv :=
  (map (fun T => (typeSubst_in_type T k R)) G)
.

Theorem Type_substitution_preserves_typing_cor1:
  forall (D: TypeEnv) (G: TermEnv) (Pi R T: TypeS) (k: KindS) (t: Term),
    (Type_WK D R (TypeTuple k)) ->
    (SectionSat D R Pi) ->
    let D' := (snoc D Pi) in
    (TypeEnv_WK D') ->
    (TermEnv_WK D' G) ->
    (Term_WT D' G t (TermI T)) ->
    (Term_WT D
             (typeSubst_in_termEnv G 0 R)
             (typeSubst_in_term t 0 R)
             (TermI (typeSubst_in_type T 0 R)))
.


Theorem Type_substitution_preserves_typing_cor2:
  forall (D: TypeEnv) (G: TermEnv) (Pi R T: TypeS) (k: KindS) (t: Term),
    (Type_WK nil R (TypeTuple k)) ->
    (SectionSat nil R Pi) ->
    let D' := (Pi :: D) in
    (TypeEnv_WK D') ->
    (TermEnv_WK D' G) ->
    (Term_WT D' G t (TermI T)) ->
    (Term_WT (typeSubst_in_typeEnv D 0 R)
             (typeSubst_in_termEnv G (length D) R)
             (typeSubst_in_term t (length D) R)
             (TermI (typeSubst_in_type T (length D) R)))
.


Theorem Type_substitution_preserves_typing_cor3:
  forall (G: TermEnv) (Pi Pi' R T: TypeS) (k: KindS) (t: Term),
    (Type_WK nil R (TypeTuple k)) ->
    (SectionSat nil R Pi) ->
    let D := (Pi :: Pi' :: nil) in
    (TypeEnv_WK D) ->
    (TermEnv_WK D G) ->
    (Term_WT D G t (TermI T)) ->
    (Term_WT ((typeSubst_in_type Pi' 0 R) :: nil)
             (typeSubst_in_termEnv G 1 R)
             (typeSubst_in_term t 1 R)
             (TermI (typeSubst_in_type T 1 R)))
.


Theorem Type_substitution_preserves_typing_cor4:
  forall (Us: TermEnv) (Pi Pi' R T U: TypeS) (k: KindS) (t: Term),
    (Type_WK nil R (TypeTuple k)) ->
    (SectionSat nil R Pi) ->
    let D := (Pi :: Pi' :: nil) in
    let G := (U :: Us) in
    (TypeEnv_WK D) ->
    (TermEnv_WK D G) ->
    (Term_WT D G t (TermI T)) ->
    (Term_WT ((typeSubst_in_type Pi' 0 R) :: nil)
             ((typeSubst_in_type U 1 R) :: (typeSubst_in_termEnv Us 1 R))
             (typeSubst_in_term t 1 R)
             (TermI (typeSubst_in_type T 1 R)))
.


Theorem Type_substitution_preserves_typing_cor5:
  forall (G: TermEnv) (Pi R T: TypeS) (k: KindS) (t: Term),
    (Type_WK nil R (TypeTuple k)) ->
    (SectionSat nil R Pi) ->
    let D := (Pi :: nil) in
    (TypeEnv_WK D) ->
    (TermEnv_WK D G) ->
    (Term_WT D G t (TermI T)) ->
    (Term_WT nil
             (typeSubst_in_termEnv G 0 R)
             (typeSubst_in_term t 0 R)
             (TermI (typeSubst_in_type T 0 R)))
.


End SetProgram.