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.CtxConversion
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.Equiv
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.Validity
.
Require
Import
Lambda.TPOSR.TypesDepth
.
Require
Import
Lambda.TPOSR.TypesFunctionality
.
Require
Import
Lambda.TPOSR.UniquenessOfTypes
.
Require
Import
Lambda.TPOSR.ChurchRosserDepth
.
Require
Import
Lambda.TPOSR.ChurchRosser
.
Require
Import
Lambda.TPOSR.SubjectReduction
.
Require
Import
Lambda.TPOSR.Unlab
.
Require
Import
Lambda.TPOSR.TPOSR_trans
.
Require
Import
Lambda.TPOSR.UnlabConv
.
Require
Import
Lambda.Terms
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.InvLiftSubst
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Russell.Types
.
Ltac
destruct_lab_inv
c
H
:=
destruct
c
; try
discriminate
; simpl
in
H
; inversion
H
; subst
.
Lemma
unlab_ctx_item
: ∀ a
x
n
,
item
term
x
(unlab_ctx
a
) n
->
∃ x'
, item
lterm
x'
a
n
∧ (|x'|) = x
.
Theorem
russell_to_tposr
:
(∀ G
M
T
, G
|-- M
: T
->
exists3
G'
M'
T'
, unlab_ctx
G'
= G
∧ (|M'|) = M
∧ (|T'|) = T
∧
G'
|-- M'
-> M'
: T'
) ∧
(∀ G
t
u
s
, G
|-- t
>> u
: s
->
exists3
G'
t'
u'
, unlab_ctx
G'
= G
∧ (| t'
|) = t
∧ (| u'
|) = u
∧
G'
|-- t'
>-> u'
: s
) ∧
(∀ G
, wf
G
-> ∃ G'
, unlab_ctx
G'
= G
∧ tposr_wf
G'
∧
(∀ T
n
, Env.item_lift
T
G
n
->
∃ T'
, item_llift
T'
G'
n
∧ (|T'|) = T
)).
Corollary
type_russell_tposr
:
∀ G
M
T
, G
|-- M
: T
->
exists3
G'
M'
T'
, unlab_ctx
G'
= G
∧ (|M'|) = M
∧ (|T'|) = T
∧
G'
|-- M'
-> M'
: T'
.
Corollary
coerce_russell_tposr
:
∀ G
t
u
s
, G
|-- t
>> u
: s
->
exists3
G'
t'
u'
, unlab_ctx
G'
= G
∧ (| t'
|) = t
∧ (| u'
|) = u
∧
G'
|-- t'
>-> u'
: s
.
Corollary
wf_russell_tposr
:
∀ G
, wf
G
-> ∃ G'
, unlab_ctx
G'
= G
∧ tposr_wf
G'
.
Lemma
conv_eq2
: ∀ t
u
, conv
(|t|) (|u|) ->
∀ e
(s
s'
: sort
), e
|-- t
-> t
: s
-> e
|-- u
-> u
: s'
-> s
= s'
.
Corollary
russell_unique_sort_conv
: ∀ G
A
A'
s1
s2
,
G
|-- A
: Srt
s1
-> G
|-- A'
: Srt
s2
-> conv
A
A'
-> s1
= s2
.