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.Generation
.
Require
Import
Lambda.TPOSR.TypesDepth
.
Lemma
pi_conv_right_aux
:
∀ G'
X
Y
Y'
s2
, G'
|-- Y
~= Y'
: s2
->
∀ G
, G'
= X
:: G
->
∀ s1
, G
|-- X
-> X
: Srt_l
s1
->
G
|-- Prod_l
X
Y
~= Prod_l
X
Y'
: s2
.
Lemma
pi_conv_right
:
∀ G
X
s1
, G
|-- X
-> X
: Srt_l
s1
->
∀ Y
Y'
s2
, X
:: G
|-- Y
~= Y'
: s2
->
G
|-- Prod_l
X
Y
~= Prod_l
X
Y'
: s2
.
Lemma
pi_conv_left
:
∀ G
X
X'
s1
, G
|-- X
~= X'
: s1
->
∀ Y
s2
, X
:: G
|-- Y
-> Y
: Srt_l
s2
->
G
|-- Prod_l
X
Y
~= Prod_l
X'
Y
: s2
.
Theorem
pi_functionality
: ∀ G
X
X'
s1
, G
|-- X
~= X'
: s1
->
∀ Y
Y'
s2
, X
:: G
|-- Y
~= Y'
: s2
->
G
|-- Prod_l
X
Y
~= Prod_l
X'
Y'
: s2
.
Lemma
sum_conv_right_aux
:
∀ G'
X
Y
Y'
s2
, G'
|-- Y
~= Y'
: s2
->
∀ G
, G'
= X
:: G
->
∀ s1
, G
|-- X
-> X
: Srt_l
s1
->
∀ s3
, sum_sort
s1
s2
s3
->
G
|-- Sum_l
X
Y
~= Sum_l
X
Y'
: s3
.
Lemma
sum_conv_right
:
∀ G
X
s1
, G
|-- X
-> X
: Srt_l
s1
->
∀ Y
Y'
s2
, X
:: G
|-- Y
~= Y'
: s2
->
∀ s3
, sum_sort
s1
s2
s3
->
G
|-- Sum_l
X
Y
~= Sum_l
X
Y'
: s3
.
Lemma
sum_conv_left
:
∀ G
X
X'
s1
, G
|-- X
~= X'
: s1
->
∀ Y
s2
, X
:: G
|-- Y
-> Y
: Srt_l
s2
->
∀ s3
, sum_sort
s1
s2
s3
->
G
|-- Sum_l
X
Y
~= Sum_l
X'
Y
: s3
.
Theorem
sigma_functionality
: ∀ G
X
X'
s1
, G
|-- X
~= X'
: s1
->
∀ Y
Y'
s2
, X
:: G
|-- Y
~= Y'
: s2
->
∀ s3
, sum_sort
s1
s2
s3
->
G
|-- Sum_l
X
Y
~= Sum_l
X'
Y'
: s3
.
Lemma
subset_conv_right_aux
:
∀ G'
X
Y
Y'
s
, G'
|-- Y
~= Y'
: s
->
s
= prop
->
∀ G
, G'
= X
:: G
-> G
|-- X
-> X
: Srt_l
set
->
G
|-- Subset_l
X
Y
~= Subset_l
X
Y'
: set
.
Lemma
subset_conv_right
:
∀ G
X
, G
|-- X
-> X
: Srt_l
set
->
∀ Y
Y'
, X
:: G
|-- Y
~= Y'
: prop
->
G
|-- Subset_l
X
Y
~= Subset_l
X
Y'
: set
.
Lemma
subset_conv_left
:
∀ G
X
X'
s
, G
|-- X
~= X'
: s
->
s
= set
->
∀ Y
, X
:: G
|-- Y
-> Y
: Srt_l
prop
->
G
|-- Subset_l
X
Y
~= Subset_l
X'
Y
: set
.
Lemma
subset_functionality_aux
:
∀ G
X
X'
s
, G
|-- X
~= X'
: s
->
s
= set
->
∀ Y
Y'
, X
:: G
|-- Y
~= Y'
: prop
->
G
|-- Subset_l
X
Y
~= Subset_l
X'
Y'
: set
.
Corollary
subset_functionality
:
∀ G
X
X'
, G
|-- X
~= X'
: set
->
∀ Y
Y'
, X
:: G
|-- Y
~= Y'
: prop
->
G
|-- Subset_l
X
Y
~= Subset_l
X'
Y'
: set
.