Require
Import
Lambda.Utils
.
Require
Import
Lambda.Tactics
.
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.Substitution
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.Equiv
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.ChurchRosser
.
Require
Import
Lambda.TPOSR.CoerceDepth
.
Require
Import
Lambda.TPOSR.Transitivity
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: lterm
.
Corollary
injectivity_of_pi_coerce_rc_depth_aux
: ∀ e
T
U
s
n
,
e
|-- T
>-> U
: s
[n
] ->
∀ A
A'
B
B'
, e
|-- T
~= Prod_l
A
B
: s
-> e
|-- U
~= Prod_l
A'
B'
: s
->
∃ s1
, e
|-- A'
>-> A
: s1
∧ A'
:: e
|-- B
>-> B'
: s
.
Corollary
injectivity_of_pi_coerce
: ∀ e
A
A'
B
B'
s
,
e
|-- Prod_l
A
B
>-> Prod_l
A'
B'
: s
->
∃ s1
, e
|-- A'
>-> A
: s1
∧ A'
:: e
|-- B
>-> B'
: s
.
Corollary
injectivity_of_sum_coerce_rc_depth_aux
: ∀ e
T
U
s
n
,
e
|-- T
>-> U
: s
[n
] ->
∀ A
A'
B
B'
, e
|-- T
~= Sum_l
A
B
: s
-> e
|-- U
~= Sum_l
A'
B'
: s
->
exists2
s1
s2
, e
|-- A
>-> A'
: s1
∧ A
:: e
|-- B
>-> B'
: s2
∧
sum_sort
s1
s2
s
.
Corollary
injectivity_of_sum_coerce
: ∀ e
A
A'
B
B'
s
,
e
|-- Sum_l
A
B
>-> Sum_l
A'
B'
: s
->
exists2
s1
s2
, e
|-- A
>-> A'
: s1
∧ A
:: e
|-- B
>-> B'
: s2
∧ sum_sort
s1
s2
s
.