Require
Import
Lambda.Utils
.
Require
Import
Lambda.Tactics
.
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.Basic
.
Require
Import
Lambda.TPOSR.Thinning
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.Equiv
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.TypesDepth
.
Theorem
ind_validity
: ∀ n
,
∀ e
t
u
T
, e
|-- t
-> u
: T
[n
] ->
(∃ s
, T
= Srt_l
s
) ∨
(exists2
T'
s
, e
|-- T
-> T'
: Srt_l
s
).
Corollary
validity
: ∀ e
t
u
T
, e
|-- t
-> u
: T
->
(∃ s
, T
= Srt_l
s
) ∨
(exists2
T'
s
, e
|-- T
-> T'
: Srt_l
s
).
Corollary
validity_tposrp
: ∀ e
t
u
T
, e
|-- t
-+> u
: T
->
(∃ s
, T
= Srt_l
s
) ∨
(exists2
T'
s
, e
|-- T
-> T'
: Srt_l
s
).