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
.
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
wf_is_sorted
: ∀ e
, wf
e
→
∀ x
n
, item
_
x
e
n
→ ∀ s
, x
= Srt
s
→ is_prop
s
.
Lemma
inv_lift_sort
: ∀ t
s
n
, lift
n
t
= Srt
s
→ t
= Srt
s
.
Lemma
inv_subst_sort
: ∀ t
t'
n
s
, subst_rec
t
t'
n
= Srt
s
→
t
= Srt
s
∨ t'
= Srt
s
.
Lemma
gen_sorting_var_aux
: ∀ e
t
T
, e
|-- t
: T
→
∀ n
, t
= Ref
n
→
∀ s
, T
= (Srt
s
) →
is_prop
s
.
Lemma
gen_sorting_var
:
∀ e
n
s
, e
|-- Ref
n
: Srt
s
→ is_prop
s
.
Lemma
gen_sorting_app_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
N
, t
= App
M
N
→
∀ s
, Ts
= Srt
s
→ is_prop
s
.
Lemma
gen_sorting_app
: ∀ e
M
N
s
, e
|-- App
M
N
: Srt
s
→ is_prop
s
.
Lemma
gen_sorting_pi1_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
, t
= Pi1
M
→
∀ s
, Ts
= Srt
s
→ is_prop
s
.
Lemma
gen_sorting_pi1
: ∀ e
M
s
, e
|-- Pi1
M
: Srt
s
→ is_prop
s
.
Lemma
gen_sorting_pi2_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
, t
= Pi2
M
→
∀ s
, Ts
= Srt
s
→ is_prop
s
.
Lemma
gen_sorting_pi2
: ∀ e
M
s
, e
|-- Pi2
M
: Srt
s
→ is_prop
s
.
Lemma
sorting_lambda_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ T
M
, t
= Abs
T
M
→ ∀ s
, Ts
≠ Srt
s
.
Lemma
sorting_lambda
: ∀ e
T
M
s
, ¬ e
|-- Abs
T
M
: Srt
s
.
Lemma
generation_prod_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Prod
U
V
→ ∃ s
, Ts
= Srt
s
.
Lemma
generation_prod
: ∀ e
U
V
Ts
, e
|-- Prod
U
V
: Ts
→
∃ s
, Ts
= Srt
s
.
Lemma
generation_prod2_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Prod
U
V
→ ∀ s
, Ts
= Srt
s
→
(∃ s'
, e
|-- U
: Srt
s'
) ∧ (U
:: e
) |-- V
: Srt
s
.
Lemma
generation_prod2
: ∀ e
U
V
s
, e
|-- Prod
U
V
: Srt
s
→
(∃ s'
, e
|-- U
: Srt
s'
) ∧ (U
:: e
) |-- V
: Srt
s
.
Lemma
generation_sum_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Sum
U
V
→ ∃ s
, Ts
= Srt
s
.
Lemma
generation_sum
: ∀ e
U
V
Ts
, e
|-- Sum
U
V
: Ts
→
∃ s
, Ts
= Srt
s
.
Lemma
generation_sum2_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Sum
U
V
→ ∀ s
, Ts
= Srt
s
→
e
|-- U
: Srt
s
∧ (U
:: e
) |-- V
: Srt
s
∧ sum_sort
s
s
s
.
Lemma
generation_sum2
: ∀ e
U
V
s
, e
|-- Sum
U
V
: Srt
s
→
e
|-- U
: Srt
s
∧ (U
:: e
) |-- V
: Srt
s
∧ sum_sort
s
s
s
.
Lemma
generation_subset_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Subset
U
V
→ Ts
= Srt
set
.
Lemma
generation_subset
: ∀ e
U
V
Ts
, e
|-- Subset
U
V
: Ts
→
Ts
= Srt
set
.
Lemma
generation_subset2_aux
: ∀ e
T
Ts
, e
|-- T
: Ts
→
∀ U
V
, T
= Subset
U
V
→ Ts
= Srt
set
→
e
|-- U
: Srt
set
∧ (U
:: e
) |-- V
: Srt
prop
.
Lemma
generation_subset2
: ∀ e
U
V
s
, e
|-- Subset
U
V
: Srt
set
→
(e
|-- U
: Srt
set
) ∧ (U
:: e
) |-- V
: Srt
prop
.
Lemma
var_sort_item
: ∀ e
t
T
, e
|-- t
: T
→
∀ n
, t
= Ref
n
→
∀ s
, T
= (Srt
s
) → item
_
(Srt
s
) e
n
.
Lemma
unique_var_sort
: ∀ e
n
s
, e
|-- Ref
n
: Srt
s
→
∀ s'
, e
|-- Ref
n
: Srt
s'
→ s
= s'
.
Lemma
sort_of_app_aux
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
N
, t
= App
M
N
→
∀ s
, Ts
= Srt
s
→
(∃ V
, e
|-- M
: Prod
V
(Srt
s
) ∧ e
|-- N
: V
).
Lemma
sort_of_app
: ∀ e
M
N
s
, e
|-- App
M
N
: Srt
s
→
∃ V
, e
|-- M
: Prod
V
(Srt
s
) ∧ e
|-- N
: V
.
Lemma
sort_of_app_aux2
: ∀ e
t
Ts
, e
|-- t
: Ts
→
∀ M
N
, t
= App
M
N
→
∀ s
, Ts
= Srt
s
→
∀ s'
, ¬ N
= Srt
s'
.
Lemma
sort_of_app2
: ∀ e
M
N
s
, e
|-- App
M
N
: Srt
s
→ ∀ s'
, ¬ N
= Srt
s'
.
Lemma
strength_sort_judgement
: ∀ T
e
s
s'
, T
:: e
|-- Srt
s
: Srt
s'
→
e
|-- Srt
s
: Srt
s'
.
Lemma
type_sorted
: ∀ e
t
T
, e
|-- t
: T
→
T
= Srt
kind
∨ ∃ s
, e
|-- T
: Srt
s
.