Require
Import
Lambda.Utils
.
Require
Import
Lambda.Tactics
.
Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Conv_Dec
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.InvLiftSubst
.
Require
Import
Lambda.Env
.
Require
Import
Lambda.JRussell.Types
.
Require
Import
Lambda.JRussell.Basic
.
Require
Import
Lambda.JRussell.Thinning
.
Require
Import
Lambda.JRussell.Substitution
.
Require
Import
Lambda.JRussell.Coercion
.
Require
Import
Lambda.JRussell.GenerationNotKind
.
Require
Import
Lambda.JRussell.GenerationCoerce
.
Require
Import
Lambda.JRussell.Generation
.
Require
Import
Lambda.JRussell.GenerationRange
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: term
.
Implicit
Types
e
f
g
: env
.
Lemma
sum_sort_functional
: ∀ a
b
c
c'
, sum_sort
a
b
c
→ sum_sort
a
b
c'
→ c
= c'
.
Lemma
generation_prod2
: ∀ e
t
T
, e
|-= t
: T
→
∀ U
V
, t
= Prod
U
V
→
∃ s
, T
= Srt
s
∧
(∃ s'
, e
|-= U
: Srt
s'
) ∧ (U
:: e
) |-= V
: Srt
s
.
Lemma
generation_sum2
: ∀ e
t
T
, e
|-= t
: T
→
∀ U
V
, t
= Sum
U
V
→
exists3
s1
s2
s3
, T
= Srt
s3
∧
e
|-= U
: Srt
s1
∧ (U
:: e
) |-= V
: Srt
s2
∧ sum_sort
s1
s2
s3
.
Lemma
generation_subset
: ∀ e
t
T
, e
|-= t
: T
→
∀ U
V
, t
= Subset
U
V
→
T
= Srt
set
∧
e
|-= U
: Srt
set
∧ (U
:: e
) |-= V
: Srt
prop
.
Lemma
unique_range_sort
: ∀ t
e
T
T'
, e
|-= t
: T
→ e
|-= t
: T'
→
∀ s1
s2
,
(type_range
T
= Srt
s1
→ type_range
T'
= Srt
s2
→ s1
= s2
).