Library Lambda.Russell.Injectivity


Require
 Import
 Lambda.Tactics.

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.Substitution.

Require
 Import
 Lambda.Russell.Coercion.

Require
 Import
 Lambda.Russell.GenerationNotKind.

Require
 Import
 Lambda.Russell.GenerationCoerce.

Require
 Import
 Lambda.Russell.Generation.




Require
 Import
 Lambda.Meta.Russell_TPOSR.




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
 unique_sort_conv : ∀ G
 A
 A'
 s1
 s2
, G
 |-- A
 : Srt s1
 → G
 |-- A'
 : Srt s2
 → conv A
 A'
 → s1
 = s2
.




Lemma
 inv_conv_prod_sort_l : ∀ e
 U
 V
 U'
 V'
 s
, e
 |-- Prod U
 V
 : Srt s
 → e
 |-- Prod U'
 V'
 : Srt s
 →

  conv (Prod U
 V
) (Prod U'
 V'
) → ∃ s1
 : sort, e
 |-- U
 : Srt s1
 ∧ e
 |-- U'
 : Srt s1
 .




Lemma
 inv_conv_prod_sort_r : ∀ e
 U
 V
 U'
 V'
 s
, e
 |-- Prod U
 V
 : Srt s
 → e
 |-- Prod U'
 V'
 : Srt s
 →

  conv (Prod U
 V
) (Prod U'
 V'
) → U'
 :: e
 |-- V
 : Srt s
 ∧ U'
 :: e
 |-- V'
 : Srt s
.




Lemma
 inv_conv_sum_sort : ∀ e
 U
 V
 U'
 V'
 s
, e
 |-- Sum U
 V
 : Srt s
 → e
 |-- Sum U'
 V'
 : Srt s
 →

  conv (Sum U
 V
) (Sum U'
 V'
) → 

  ∃ s1
, ∃ s2
, e
 |-- U
 : Srt s1
 ∧ e
 |-- U'
 : Srt s1
 ∧ U
 :: e
 |-- V
 : Srt s2
 ∧ U
 :: e
 |-- V'
 : Srt s2


  ∧ sum_sort s1
 s2
 s
.




Require
 Import
 Lambda.Russell.UnicityOfSorting.

Versions of the lemmas usable when in Set


Lemma
 inv_conv_prod_sort_l_set : ∀ e
 U
 V
 U'
 V'
 s
, 

  e
 |-- Prod U
 V
 : Srt s
 → e
 |-- Prod U'
 V'
 : Srt s
 →

  conv (Prod U
 V
) (Prod U'
 V'
) → 

  ∀ s1
, e
 |-- U
 : Srt s1
 → e
 |-- U'
 : Srt s1
.




Lemma
 inv_conv_prod_sort_r_set : ∀ e
 U
 V
 U'
 V'
 s
, 

  e
 |-- Prod U
 V
 : Srt s
 → e
 |-- Prod U'
 V'
 : Srt s
 →

  conv (Prod U
 V
) (Prod U'
 V'
) → 

  U'
 :: e
 |-- V
 : Srt s
 ∧ U'
 :: e
 |-- V'
 : Srt s
.




Lemma
 inv_conv_sum_sort_l_set : ∀ e
 U
 V
 U'
 V'
 s
, e
 |-- Sum U
 V
 : Srt s
 → e
 |-- Sum U'
 V'
 : Srt s
 →

  conv (Sum U
 V
) (Sum U'
 V'
) → 

  ∀ s1
 : sort, e
 |-- U
 : Srt s1
 → e
 |-- U'
 : Srt s1
.




Lemma
 inv_conv_sum_sort_r_set : ∀ e
 U
 V
 U'
 V'
 s
, e
 |-- Sum U
 V
 : Srt s
 → e
 |-- Sum U'
 V'
 : Srt s
 →

  conv (Sum U
 V
) (Sum U'
 V'
) → 

  ∀ s2
 : sort, U
 :: e
 |-- V
 : Srt s2
 → U
 :: e
 |-- V'
 : Srt s2
.