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.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
.
Lemma
sum_sort_functional
: ∀ a
b
c
c'
, sum_sort
a
b
c
-> sum_sort
a
b
c'
-> c
= c'
.
Lemma
toq
: ∀ G
M
M'
A
n
, G
|-- M
-> M'
: A
[n
] -> tposr_term_depth
G
M
A
.
Theorem
uniqueness_of_types
: ∀ e
M
A
B
,
tposr_term_depth
e
M
A
-> tposr_term_depth
e
M
B
-> equiv
e
A
B
.
Corollary
tposr_uniqueness_of_types
: ∀ e
M
M'
M''
A
B
,
e
|-- M
-> M'
: A
-> e
|-- M
-> M''
: B
-> equiv
e
A
B
.
Corollary
tposrp_uniqueness_of_types
: ∀ e
M
M'
M''
A
B
,
e
|-- M
-+> M'
: A
-> e
|-- M
-+> M''
: B
-> equiv
e
A
B
.