Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Env
.
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.Thinning
.
Require
Import
Lambda.TPOSR.CtxReduction
.
Require
Import
Lambda.TPOSR.CtxExpansion
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.SubstitutionTPOSR
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Lemma
tposr_conv_eq
: ∀ e
A
B
s
, e
|-- A
~= B
: s
->
∀ M
N
, (e
|-- M
-> N
: A
-> e
|-- M
-> N
: B
) ∧ (e
|-- M
-> N
: B
-> e
|-- M
-> N
: A
).
Corollary
tposr_conv_l
: ∀ e
A
B
s
, e
|-- A
~= B
: s
->
∀ M
N
, e
|-- M
-> N
: A
-> e
|-- M
-> N
: B
.
Corollary
tposr_conv_r
: ∀ e
A
B
s
, e
|-- A
~= B
: s
->
∀ M
N
, e
|-- M
-> N
: B
-> e
|-- M
-> N
: A
.
Corollary
tposrp_conv_l
: ∀ e
A
B
s
, e
|-- A
~= B
: s
->
∀ M
N
, e
|-- M
-+> N
: A
-> e
|-- M
-+> N
: B
.
Corollary
tposrp_conv_r
: ∀ e
A
B
s
, e
|-- A
~= B
: s
->
∀ M
N
, e
|-- M
-+> N
: B
-> e
|-- M
-+> N
: A
.
Lemma
tposrp_conv
: ∀ e
A
B
s
, e
|-- A
>-> B
: s
->
∀ M
N
, e
|-- M
-+> N
: A
-> e
|-- M
-+> N
: B
.
Lemma
tposrp_tposr_eq_aux
: ∀ e
M
N
Z
, e
|-- M
-+> N
: Z
-> ∀ s
, Z
= Srt_l
s
-> e
|-- M
~= N
: s
.
Lemma
tposrp_tposr_eq
: ∀ e
M
N
s
, e
|-- M
-+> N
: Srt_l
s
-> e
|-- M
~= N
: s
.
Hint
Resolve
tposrp_tposr_eq
: coc
.
Lemma
context_validity
: ∀ g
, tposr_wf
g
-> ∀ n
d
, trunc
_
n
g
d
-> tposr_wf
d
.
Lemma
tposr_not_kind_aux
: ∀ e
t
u
T
, tposr
e
t
u
T
-> t
≠ Srt_l
kind
.
Lemma
tposr_not_kind
: ∀ e
u
T
, ¬ tposr
e
(Srt_l
kind
) u
T
.
Hint
Resolve
tposr_not_kind
: coc
.
Lemma
lsubst_to_sort
: ∀ M
N
s
, lsubst
M
N
= Srt_l
s
-> or
(M
= Srt_l
s
) (N
= Srt_l
s
).