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.PreCtxCoercion
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: lterm
.
Implicit
Types
e
f
g
: lenv
.
Inductive
coerce_in_env
: lenv
-> lenv
-> Prop
:=
| coerce_env_hd
: ∀ e
t
u
s
, e
|-- t
>-> u
: s
->
coerce_in_env
(u
:: e
) (t
:: e
)
| coerce_env_tl
:
∀ e
f
t
, tposr_wf
(t
:: f
) -> coerce_in_env
e
f
-> coerce_in_env
(t
:: e
) (t
:: f
).
Hint
Resolve
coerce_env_hd
coerce_env_tl
: coc
.
Lemma
coerce_in_env_pre
: ∀ e
f
, coerce_in_env
e
f
-> pre_coerce_in_env
e
f
.
Lemma
tposr_coerce_env
: ∀ e
t
u
T
, e
|-- t
-> u
: T
->
∀ f
, coerce_in_env
e
f
-> f
|-- t
-> u
: T
.
Lemma
eq_coerce_env
: ∀ e
T
U
s
, e
|-- T
~= U
: s
->
∀ f
, coerce_in_env
e
f
-> f
|-- T
~= U
: s
.
Lemma
coerce_coerce_env
: ∀ e
T
U
s
, e
|-- T
>-> U
: s
->
∀ f
, coerce_in_env
e
f
-> f
|-- T
>-> U
: s
.
Corollary
tposrp_coerce_env
: ∀ e
t
u
T
, e
|-- t
-+> u
: T
->
∀ f
, coerce_in_env
e
f
-> f
|-- t
-+> u
: T
.
Hint
Resolve
tposr_coerce_env
eq_coerce_env
coerce_coerce_env
: ecoc
.
Lemma
coerce_in_env_sym
: ∀ e
f
, coerce_in_env
e
f
-> coerce_in_env
f
e
.
Hint
Resolve
coerce_in_env_sym
: coc
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.PreSubstitutionTPOSR
.
Lemma
substitution_coerce_tposrp
:
∀ e
d
d'
t
, e
|-- d
-+> d'
: t
->
∀ u
v
s
, t
:: e
|-- u
>-> v
: s
-> e
|-- (lsubst
d
u
) >-> (lsubst
d'
v
) : s
.