Require
Import
Lambda.Utils
.
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.RightReflexivity
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.ChurchRosser
.
Require
Import
Lambda.TPOSR.CoerceNoTrans
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: lterm
.
Require
Import
Omega
.
Require
Import
Coq.Arith.Max
.
Lemma
depth_prod_prod_l
: ∀ n0
n1
n2
n3
,
n3
+ n2
< S
(max
n2
n1
+ S
(max
n3
n0
)).
Lemma
depth_prod_prod_r
: ∀ n0
n1
n2
n3
, n3
+ n1
< S
(max
n0
n3
+ S
(max
n2
n1
)).
Lemma
depth_prod_conv_prod
:
∀ n0
n1
n2
n3
, n3
+ S
n2
< S
(max
n2
n1
+ S
(S
(max
n3
n0
))).
Lemma
depth_prod_conv_prod2
: ∀ n0
n1
n2
n3
, n1
+ S
n0
< S
(max
n2
n1
+ S
(S
(max
n3
n0
))).
Lemma
depth_sum_conv_sum
: ∀ n0
n1
n2
n3
, S
(n3
+ n2
) < S
(max
n2
n1
+ S
(S
(max
n3
n0
))).
Lemma
depth_sum_conv_sum2
: ∀ n0
n1
n2
n3
, n3
+ S
n2
< S
(max
n3
n1
+ S
(S
(max
n2
n0
))).
Lemma
depth_conv_prod
: ∀ n0
n1
n2
n3
, S
(n3
+ n2
) < S
(S
(max
n2
n1
+ (S
(max
n3
n0
)))).
Lemma
depth_conv_prod2
: ∀ n0
n1
n2
n3
, S
(n1
+ n3
) < S
(S
(max
n2
n1
+ S
(max
n0
n3
))).
Lemma
depth_conv_sum
: ∀ n0
n1
n2
n3
, S
(n3
+ n2
) < S
(S
(max
n3
n0
+ S
(max
n2
n1
))).
Lemma
depth_conv_sum2
: ∀ n0
n1
n2
n3
, n3
+ S
n2
< S
(S
(max
n1
n3
+ S
(max
n0
n2
))).
Lemma
coerces_sort_l
: ∀ e
T
U
s
, e
|-- T
>>> U
: s
-> e
|-- T
-> T
: s
.
Lemma
coerces_sort_r
: ∀ e
T
U
s
, e
|-- T
>>> U
: s
-> e
|-- U
-> U
: s
.
Theorem
coerce_trans_aux
: ∀ n
: nat
,
(∀ e
A
B
s
, ∀ d1
: e
|-- A
>>> B
: s
,
∀ C
, ∀ d2
: e
|-- B
>>> C
: s
,
n
= (depth
d1
) + (depth
d2
) ->
e
|-- A
>>> C
: s
).