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.Types
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.SubjectReduction
.
Require
Import
Lambda.TPOSR.Unlab
.
Require
Import
Lambda.Meta.TPOSR_JRussell
.
Require
Import
Lambda.Meta.JRussell_Russell
.
Require
Import
Lambda.Meta.Russell_JRussell
.
Require
Import
Lambda.Meta.Russell_TPOSR
.
Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.JRussell.Types
.
Require
Import
Lambda.JRussell.Validity
.
Lemma
jrussell_subject_reduction
:
∀ e
t
T
, e
|-= t
: T
-> ∀ u
, red
t
u
->
e
|-= t
= u
: T
.
Require
Import
Lambda.Russell.Types
.
Lemma
russell_subject_reduction
:
∀ e
t
T
, e
|-- t
: T
-> ∀ u
, red
t
u
->
e
|-- u
: T
.