Library Lambda.Russell.UnicityOfSorting


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.Conv_Dec.

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.Russell.GenerationRange.

Require
 Import
 Lambda.Russell.UnicityOfSortingRange.




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.







Theorem
 unique_sort : ∀ t
 e
 s
 s'
, 

  e
 |-- t
 : (Srt s
) → e
 |-- t
 : (Srt s'
) → s
 = s'
.




Lemma
 any_sort_coerce_l : ∀ e
 U
 V
 s
, e
 |-- U
 >> V
 : s
 → ∀ s'
,

  e
 |-- U
 : Srt s'
 → e
 |-- U
 >> V
 : s'
.




Lemma
 any_sort_coerce_r : ∀ e
 U
 V
 s
, e
 |-- U
 >> V
 : s
 → ∀ s'
,

  e
 |-- V
 : Srt s'
 → e
 |-- U
 >> V
 : s'
.