Require Import List.
Require Import Relations.
Require Import Arith.

Require Import MatchCompNat.

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

Require Substitutions_proofs.
Module My_Substitutions_proofs := Substitutions_proofs.SetProgram(My_Program).
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.


Require Import Peano_dec.

Lemma Type_eqdec:
  forall (t u: TypeS),
    { t = u } + { t <> u }
.


Lemma TypeS_at_is_a_partial_function:
  forall (ts t t': TypeS) (i: nat),
    (TypeS_at ts i t) ->
    (TypeS_at ts i t') ->
    (t = t')
.




Lemma TypeS_at_of_typeSubst:
  forall (ts ti R: TypeS) (X: TypeVar) (i: nat),
  (TypeS_at ts i ti) ->
  (TypeS_at (typeSubst_in_type ts X R) i (typeSubst_in_type ti X R))
.




Lemma TypeS_at_of_lift:
  forall (ts ti: TypeS) (n k i: nat),
  (TypeS_at ts i ti) ->
  (TypeS_at (lift_at_depth_in_type ts n k) i (lift_at_depth_in_type ti n k))
.




Lemma Substitution_in_reduction:
  forall (R t t': TypeS),
    (RedType t t') ->
    forall (k: nat),
      (RedType (typeSubst_in_type t k R) (typeSubst_in_type t' k R))
.



















Inductive RedTypeStar: TypeS -> TypeS -> Prop :=
  | RedType_step: forall (t t': TypeS), (RedType t t') -> (RedTypeStar t t')
  | RedType_refl: forall (t: TypeS), (RedTypeStar t t)
  | RedType_trans: forall (t u t': TypeS), (RedTypeStar t u) -> (RedTypeStar u t') ->
    (RedTypeStar t t')
.

Inductive RedTypeEnvStar: TypeEnv -> TypeEnv -> Prop :=
  | RedTypeEnv_step: forall (D D': TypeEnv), (RedTypeEnv D D') -> (RedTypeEnvStar D D')
  | RedTypeEnv_refl: forall (D: TypeEnv), (RedTypeEnvStar D D)
  | RedTypeEnv_trans: forall (D1 D2 D3: TypeEnv), (RedTypeEnvStar D1 D2) ->
    (RedTypeEnvStar D2 D3) -> (RedTypeEnvStar D1 D3)
.


Lemma RTS_proj_sub:
  forall (R R': TypeS) (i: nat),
    (RedTypeStar R R') ->
    (RedTypeStar (Type_proj R i) (Type_proj R' i))
.




Lemma RTS_fun_left:
  forall (Pi Pi' T: TypeS),
    (RedTypeStar Pi Pi') ->
    (RedTypeStar (Type_fun Pi T) (Type_fun Pi' T))
.




Lemma RTS_fun_right:
  forall (Pi T T': TypeS),
    (RedTypeStar T T') ->
    (RedTypeStar (Type_fun Pi T) (Type_fun Pi T'))
.




Lemma RTS_apply_left:
  forall (K K' R: TypeS),
    (RedTypeStar K K') ->
    (RedTypeStar (Type_apply K R) (Type_apply K' R))
.




Lemma RTS_apply_right:
  forall (K R R': TypeS),
    (RedTypeStar R R') ->
    (RedTypeStar (Type_apply K R) (Type_apply K R'))
.




Lemma RTS_tuple:
  forall (Ks Ks': TypeS),
    (RedTypeStar Ks Ks') ->
    (RedTypeStar (Type_tuple Ks) (Type_tuple Ks'))
.




Lemma RTS_param_left:
  forall (Pi Pi' T: TypeS),
    (RedTypeStar Pi Pi') ->
    (RedTypeStar (Type_param Pi T) (Type_param Pi' T))
.




Lemma RTS_param_right:
  forall (Pi T T': TypeS),
    (RedTypeStar T T') ->
    (RedTypeStar (Type_param Pi T) (Type_param Pi T'))
.




Lemma RTS_section:
  forall (Ps Ps': TypeS),
    (RedTypeStar Ps Ps') ->
    (RedTypeStar (Type_section Ps) (Type_section Ps'))
.




Lemma RTS_some:
  forall (T T': TypeS),
    (RedTypeStar T T') ->
    (RedTypeStar (Type_some T) (Type_some T'))
.




Lemma RTS_cons_head:
  forall (t t' ts: TypeS),
    (RedTypeStar t t') ->
    (RedTypeStar (Type_cons t ts) (Type_cons t' ts))
.




Lemma RTS_cons_tail:
  forall (t ts ts': TypeS),
    (RedTypeStar ts ts') ->
    (RedTypeStar (Type_cons t ts) (Type_cons t ts'))
.




Lemma Reduction_in_lifting:
  forall (t t': TypeS) (n: nat),
    (RedType t t') ->
    forall (k: nat),
      (RedType (lift_at_depth_in_type t n k) (lift_at_depth_in_type t' n k))
.





















Lemma Reduction_in_substitution:
  forall (R R': TypeS),
    (RedType R R') ->
    forall (t: TypeS) (k: nat),
      (RedTypeStar (typeSubst_in_type t k R) (typeSubst_in_type t k R'))
.


























Lemma Substitution_in_reduction_star:
  forall (R t t': TypeS) (k: nat),
    (RedTypeStar t t') ->
    (RedTypeStar (typeSubst_in_type t k R) (typeSubst_in_type t' k R))
.




Lemma Reduction_in_substitution_star:
  forall (R R': TypeS) (t: TypeS) (k: nat),
    (RedTypeStar R R') ->
    (RedTypeStar (typeSubst_in_type t k R) (typeSubst_in_type t k R'))
.




Lemma Reduction_and_substitution_star:
  forall (t t' R R': TypeS) (k: nat),
    (RedTypeStar t t') ->
    (RedTypeStar R R') ->
    (RedTypeStar (typeSubst_in_type t k R) (typeSubst_in_type t' k R'))
.



Lemma Subclass_implies_class_expansion:
  forall (C C': ClassSym) (R: TypeS),
  (Subclass C C') ->
  exists R': TypeS,
    (Class_subtyping (Class_type C R) (Class_type C' R'))
.





End SetProgram.