Require
Import
Lambda.JRussell.Types
.
Require
Import
Lambda.JRussell.Validity
.
Require
Import
Lambda.Russell.Types
.
Require
Import
Lambda.Russell.Thinning
.
Require
Import
Lambda.Russell.Coercion
.
Require
Import
Lambda.Russell.Substitution
.
Require
Import
Lambda.Russell.Inversion
.
Require
Import
Lambda.Russell.Generation
.
Require
Import
Lambda.Russell.GenerationRange
.
Require
Import
Lambda.Russell.UnicityOfSorting
.
Require
Import
Lambda.Russell.Transitivity
.
Require
Import
Lambda.Terms
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Env
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: term
.
Theorem
jrussell_to_russell
:
(∀ G
t
T
, G
|-= t
: T
-> G
|-- t
: T
) ∧
(∀ G
U
V
s
, G
|-= U
>> V
: s
-> G
|-- U
: Srt
s
∧ G
|-- V
: Srt
s
∧
G
|-- U
>> V
: s
) ∧
(∀ G
u
v
T
, G
|-= u
= v
: T
-> G
|-- u
: T
∧ G
|-- v
: T
∧
conv
u
v
).
Corollary
type_jrussell_to_russell
: ∀ G
t
T
, Lambda.JRussell.Types.typ
G
t
T
-> G
|-- t
: T
.
Corollary
coerce_jrussell_to_russell
: ∀ G
U
V
s
,
Lambda.JRussell.Types.coerce
G
U
V
s
-> G
|-- U
>> V
: s
.
Corollary
jeq_jrussell_to_russell
: ∀ G
u
v
T
, G
|-= u
= v
: T
->
G
|-- u
: T
∧ G
|-- v
: T
∧ conv
u
v
.
Corollary
jeq_unique_sort
: ∀ G
u
s
s'
, G
|-= u
: Srt
s
-> G
|-= u
: Srt
s'
-> s
= s'
.