Require
Import
Lambda.Utils
.
Require
Import
Lambda.Tactics
.
Require
Import
Lambda.MyList
.
Require
Import
Lambda.TPOSR.Terms
.
Require
Import
Lambda.TPOSR.Reduction
.
Require
Import
Lambda.TPOSR.Conv
.
Require
Import
Lambda.TPOSR.LiftSubst
.
Require
Import
Lambda.TPOSR.Env
.
Require
Import
Lambda.TPOSR.Types
.
Require
Import
Lambda.TPOSR.Basic
.
Require
Import
Lambda.TPOSR.Thinning
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.SubstitutionTPOSR
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.Equiv
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.TypesDepth
.
Require
Import
Lambda.TPOSR.Validity
.
Require
Import
Lambda.TPOSR.TypesFunctionality
.
Require
Import
Lambda.TPOSR.UniquenessOfTypes
.
Require
Import
Lambda.TPOSR.ChurchRosserDepth
.
Require
Import
Lambda.TPOSR.ChurchRosser
.
Require
Import
Lambda.TPOSR.Injectivity
.
Theorem
subject_reduction_depth
: ∀ t
t'
, par_lred1
t
t'
-> ∀ e
T
, tposr_term_depth
e
t
T
->
tposr
e
t
t'
T
.
Corollary
subject_reduction
: ∀ t
t'
, par_lred1
t
t'
-> ∀ e
T
, tposr_term
e
t
T
->
e
|-- t
-> t'
: T
.
Corollary
subject_reduction_p
: ∀ t
t'
, par_lred
t
t'
->
∀ e
T
, tposr_term
e
t
T
->
tposrp
e
t
t'
T
.