Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Conv_Dec
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Env
.
Require
Import
Lambda.Russell.Types
.
Require
Import
Lambda.Russell.Thinning
.
Require
Import
Lambda.Russell.Substitution
.
Require
Import
Lambda.Russell.Coercion
.
Require
Import
Lambda.Russell.GenerationNotKind
.
Require
Import
Lambda.Russell.GenerationCoerce
.
Require
Import
Lambda.Russell.Generation
.
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
type_range_lift
: ∀ n
t
k
s
, type_range
(lift_rec
n
t
k
) = Srt
s
→
type_range
t
= Srt
s
.
Lemma
type_range_subst
: ∀ t
u
n
s
, type_range
(subst_rec
t
u
n
) = Srt
s
→
type_range
t
= Srt
s
∨ type_range
u
= Srt
s
.
Lemma
no_sort_type_range
: ∀ A
, no_sort
A
→ ∀ s
, type_range
A
≠ Srt
s
.
Lemma
term_type_range_kinded
: ∀ e
t
T
, e
|-- t
: T
→
∀ s
, type_range
t
= Srt
s
→ T
= Srt
kind
.
Lemma
term_type_range_not_kind
: ∀ e
t
T
, e
|-- t
: T
→
∀ s
, type_range
t
= Srt
s
→ s
≠ kind
.
Lemma
conv_dom
:
∀ A
B
, conv
A
B
→
∀ s'
,
is_low_full
A
→ is_low_full
B
→
(type_range
A
= Srt
s'
→ type_range
B
= Srt
s'
).
Lemma
type_range_sub
: ∀ e
T
U
s
, e
|-- T
>> U
: s
→
∀ s0
, (type_range
U
= Srt
s0
→ type_range
T
= Srt
s0
).
Lemma
var_sort_range_item_aux
: ∀ e
t
T
, e
|-- t
: T
→
∀ n
, t
= Ref
n
→
∀ s
, type_range
T
= (Srt
s
) →
∃ T'
, item_lift
T'
e
n
∧ type_range
T'
= Srt
s
.
Lemma
var_sort_range_item
: ∀ e
n
T
, e
|-- Ref
n
: T
→
∀ s
, type_range
T
= (Srt
s
) →
∃ T'
, item_lift
T'
e
n
∧ type_range
T'
= Srt
s
.
Lemma
unique_var_range_sort
: ∀ e
n
T
, e
|-- Ref
n
: T
→
∀ s
, type_range
T
= Srt
s
→
∀ T'
, e
|-- Ref
n
: T'
→
∀ s'
, type_range
T'
= Srt
s'
→ s
= s'
.
Lemma
sort_of_app_range_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
N
, t
= App
M
N
→
∀ s
, type_range
Ts
= Srt
s
→
∃ V
, ∃ T
, e
|-- N
: V
∧ e
|-- M
: Prod
V
T
∧
(type_range
T
= (Srt
s
) ∨ type_range
N
= Srt
s
).
Lemma
sort_of_app_range
: ∀ e
M
N
Ts
, e
|-- App
M
N
: Ts
→
∀ s
, type_range
Ts
= Srt
s
→
∃ V
, ∃ T
, e
|-- N
: V
∧ e
|-- M
: Prod
V
T
∧
(type_range
T
= (Srt
s
) ∨ type_range
N
= Srt
s
).
Lemma
sort_of_abs_range_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
N
, t
= Abs
M
N
→
∀ s
, type_range
Ts
= Srt
s
→
∃ s1
, ∃ s2
, ∃ T
, e
|-- M
: (Srt
s1
) ∧ M
:: e
|-- N
: T
∧
M
:: e
|-- T
: Srt
s2
∧ type_range
T
= (Srt
s
).
Lemma
sort_of_abs_range
: ∀ e
M
N
Ts
, e
|-- Abs
M
N
: Ts
→
∀ s
, type_range
Ts
= Srt
s
→
∃ s1
, ∃ s2
, ∃ T
, e
|-- M
: (Srt
s1
) ∧ M
:: e
|-- N
: T
∧
M
:: e
|-- T
: Srt
s2
∧ type_range
T
= (Srt
s
).
Lemma
sort_of_pair_range_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ T
u
v
, t
= Pair
T
u
v
→
∀ s
, type_range
Ts
≠ Srt
s
.
Lemma
sort_of_pair_range
: ∀ e
T
u
v
Ts
, e
|-- Pair
T
u
v
: Ts
→
∀ s
, type_range
Ts
≠ Srt
s
.
Lemma
sum_sort_prop
: ∀ s
s'
s''
, sum_sort
s
s'
s''
→
is_prop
s
∧ s
= s'
∧ s'
= s''
.
Lemma
sort_of_sum_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Sum
U
V
→
(∀ s
, type_range
U
≠ Srt
s
) ∧
(∀ s
, type_range
V
≠ Srt
s
).
Lemma
sort_of_sum
: ∀ e
U
V
T
, e
|-- Sum
U
V
: T
→
(∀ s
, type_range
U
≠ Srt
s
) ∧
(∀ s
, type_range
V
≠ Srt
s
).
Lemma
sort_of_pi1_range_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ u
, t
= Pi1
u
→
∀ s
, type_range
Ts
≠ Srt
s
.
Lemma
sort_of_pi1_range
: ∀ e
t
Ts
, e
|-- Pi1
t
: Ts
→
∀ s
, type_range
Ts
≠ Srt
s
.
Lemma
sort_of_pi2_range_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ u
, t
= Pi2
u
→
∀ s
, type_range
Ts
≠ Srt
s
.
Lemma
sort_of_pi2_range
: ∀ e
t
Ts
, e
|-- Pi2
t
: Ts
→
∀ s
, type_range
Ts
≠ Srt
s
.
Lemma
type_range_subst2
: ∀ t
u
n
s
, type_range
t
= Srt
s
→
type_range
(subst_rec
u
t
n
) = Srt
s
.