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.SubstitutionTPOSR
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.Equiv
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.TypesDepth
.
Require
Import
Lambda.TPOSR.TypesFunctionality
.
Require
Import
Lambda.TPOSR.UniquenessOfTypes
.
Require
Import
Lambda.TPOSR.MaxLemmas
.
Implicit
Type
s
: sort
.
Lemma
tposr_tposr_coerce
: ∀ G
M
N
s
, G
|-- M
-> N
: s
-> G
|-- M
>-> N
: s
.
Lemma
tposrd_tposr_coerce
: ∀ G
M
N
s
n
, G
|-- M
-> N
: s
[n
] -> G
|-- M
>-> N
: s
.
Hint
Resolve
tposrd_tposr_coerce
: ecoc
.
Lemma
equiv_coerce_in_env
: ∀ G
M
N
s
, G
|-- M
-> M
: s
-> equiv
G
M
N
->
coerce_in_env
(M
:: G
) (N
:: G
).
Theorem
church_rosser_depth
: ∀ n
m
,
∀ G
M
N
A
, G
|-- M
-> N
: A
[n
] ->
∀ P
B
, G
|-- M
-> P
: B
[m
] ->
∃ Q
,
(G
|-- N
-> Q
: A
∧
G
|-- N
-> Q
: B
∧
G
|-- P
-> Q
: A
∧
G
|-- P
-> Q
: B
).