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.SubjectReduction
.
Require
Import
Lambda.TPOSR.Unlab
.
Require
Import
Lambda.Meta.Russell_TPOSR
.
Require
Import
Lambda.Meta.TPOSR_JRussell
.
Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Russell.Types
.
Require
Import
Lambda.JRussell.Types
.
Require
Import
Lambda.JRussell.Validity
.
Lemma
type_russell_jrussell
: ∀ e
t
T
, e
|-- t
: T
-> e
|-= t
: T
.
Lemma
conv_russell_jrussell
: ∀ e
t
u
T
,
e
|-- t
: T
-> e
|-- u
: T
-> conv
t
u
->
e
|-= t
= u
: T
.
Require
Import
Lambda.Meta.JRussell_Russell
.
Theorem
russell_equiv_jrussell_type
:
∀ e
t
T
, e
|-= t
: T
↔ e
|-- t
: T
.
Theorem
russell_equiv_jrussell_conv
:
∀ e
t
u
T
, e
|-= t
= u
: T
↔ (e
|-- t
: T
∧ e
|-- u
: T
∧ conv
t
u
).