Require
Import
Lambda.Tactics
.
Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Env
.
Require
Import
Lambda.JRussell.Types
.
Require
Import
Lambda.JRussell.Basic
.
Require
Import
Lambda.JRussell.Generation
.
Require
Import
Lambda.JRussell.Thinning
.
Require
Import
Lambda.JRussell.Validity
.
Require
Import
Lambda.Russell.Types
.
Require
Import
Lambda.Russell.UnicityOfSorting
.
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.Unlab
.
Require
Import
Lambda.Meta.JRussell_Russell
.
Require
Import
Lambda.Meta.TPOSR_JRussell
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: lterm
.
Implicit
Types
e
f
g
: lenv
.
Theorem
tposr_russell
: ∀ G
M
N
A
, G
|-- M
-> N
: A
->
(unlab_ctx
G
) |-- (|M|) : (|A|) ∧ (unlab_ctx
G
) |-- (|N|) : (|A|).
Theorem
tposr_eq_russell
: ∀ G
M
N
s
, G
|-- M
~= N
: s
->
(unlab_ctx
G
) |-- (|M|) : Srt
s
∧ (unlab_ctx
G
) |-- (|N|) : Srt
s
.
Theorem
tposr_coerce_russell
: ∀ G
M
N
s
, G
|-- M
>-> N
: s
->
(unlab_ctx
G
) |-- (|M|) : Srt
s
∧ (unlab_ctx
G
) |-- (|N|) : Srt
s
.