Require Import List.
Require Import Relations.

Require Import Util.

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

Require SubjectReduction_proofs.
Module My_SubjectReduction_proofs := SubjectReduction_proofs.SetProgram(My_Program).
Import My_SubjectReduction_proofs.

Import My_SubjectReduction_preliminaries.
Import My_TermSubstitutionInTyping.
Import My_TypeSubstitutionInTyping.
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 RedTermStar :=
  (clos_refl_trans _ RedTerm)
.

Lemma Subject_reduction_star:
  forall (t u: Term) (info: TermInfo),
    (Term_WT nil nil t info) ->
    (RedTermStar t u) ->
    exists info': TermInfo,
      (Term_WT nil nil u info') /\
      (SubInfo nil info' info)
.







Lemma Subject_reduction_star_cor1:
  forall (t t': Term) (T: TypeS),
    (Term_WT nil nil t (TermI T)) ->
    (RedTermStar t t') ->
    exists T': TypeS,
      (Term_WT nil nil t' (TermI T'))
.

Lemma Type_safety:
  forall (t: Term),
    (RedTermStar mainTerm t) ->
    (evaluated_term t) \/ (exists u: Term, (RedTerm t u))
.



End SetProgram.