Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Env
.
Require
Import
Lambda.Russell.Types
.
Require
Import
Lambda.Russell.Thinning
.
Require
Import
Lambda.Russell.Coercion
.
Require
Import
Lambda.Russell.Substitution
.
Require
Import
Lambda.Russell.Transitivity
.
Require
Import
Lambda.Russell.Inversion
.
Require
Import
Lambda.Russell.Generation
.
Require
Import
Lambda.Russell.GenerationRange
.
Require
Import
Lambda.Russell.UnicityOfSorting
.
Require
Import
Lambda.Russell.Injectivity
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: term
.
Lemma
inv_sub_prod_l_aux
: ∀ e
T
T'
s
, e
|-- T
>> T'
: s
→
∀ U
U'
V
V'
, T
= Prod
U
V
→ T'
= Prod
U'
V'
→
(∃ s1
, e
|-- U'
>> U
: s1
) ∧ U'
:: e
|-- V
>> V'
: s
.
Lemma
inv_sub_prod_l
: ∀ e
U
U'
V
V'
s
, e
|-- Prod
U
V
>> Prod
U'
V'
: s
→
∃ s1
, e
|-- U'
>> U
: s1
.
Lemma
inv_sub_prod_r
:
∀ e
U
U'
V
V'
s
, e
|-- Prod
U
V
>> Prod
U'
V'
: s
→
U'
:: e
|-- V
>> V'
: s
.
Lemma
inv_sub_sum_aux
: ∀ e
T
T'
s
, e
|-- T
>> T'
: s
→
∀ U
U'
V
V'
, T
= Sum
U
V
→ T'
= Sum
U'
V'
→
(e
|-- U
>> U'
: s
) ∧ U
:: e
|-- V
>> V'
: s
.
Lemma
inv_sub_sum_l
: ∀ e
U
U'
V
V'
s
, e
|-- Sum
U
V
>> Sum
U'
V'
: s
→
e
|-- U
>> U'
: s
.
Lemma
inv_sub_sum_r
: ∀ e
U
U'
V
V'
s
, e
|-- Sum
U
V
>> Sum
U'
V'
: s
→
U
:: e
|-- V
>> V'
: s
.
Lemma
typ_red_env
: ∀ e
U
V
s1
, e
|-- U
: Srt
s1
→ e
|-- V
: Srt
s1
→
red1
U
V
→ ∀ W
T
, U
:: e
|-- W
: T
→ V
:: e
|-- W
: T
.
Lemma
subj_red
: ∀ e
t
T
, typ
e
t
T
→ ∀ u
, red1
t
u
→ typ
e
u
T
.
Theorem
subject_reduction
:
∀ e
t
u
, red
t
u
→ ∀ T
, typ
e
t
T
→ typ
e
u
T
.