Library Lambda.Russell.Unicity


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Env.




Require
 Import
 Lambda.Russell.Types.

Require
 Import
 Lambda.Russell.Coercion.

Require
 Import
 Lambda.Russell.Inversion.

Require
 Import
 Lambda.Russell.Thinning.

Require
 Import
 Lambda.Russell.Substitution.

Require
 Import
 Lambda.Russell.Generation.

Require
 Import
 Lambda.Russell.GenerationCoerce.

Require
 Import
 Lambda.Russell.UnicityOfSorting.

Require
 Import
 Lambda.Russell.Transitivity.

Require
 Import
 Lambda.Russell.SubjectReduction.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : term.




Lemma
 type_pair_unique : ∀ e
 t
 T
, e
 |-- t
 : T
 → 

    ∀ U
 V
 u
 v
, t
 = (Pair (Sum U
 V
) u
 v
) → ∃ s
, e
 |-- (Sum U
 V
) >> T
 : s
.




Lemma
 type_pair_unique2 : ∀ e
 t
 T
, typ e
 t
 T
 →

   ∀ T'
 u
 v
, t
 = (Pair T'
 u
 v
) → ∃ U
,  ∃  V
, T'
 = Sum U
 V
.




Theorem
 typ_unique : ∀ e
 t
 T
, typ e
 t
 T
 → (∀ U
 : term, typ e
 t
 U
 → 

  ((U
 = Srt kind) ∨ (∃ s
, e
 |-- T
 >> U
 : s
))).




Lemma
 type_kind_not_conv :

  ∀ e
 t
 T
, typ e
 t
 T
 → typ e
 t
 (Srt kind) → T
 = Srt kind.




Lemma
 type_reduction :

  ∀ e
 t
 T
 (U
 : term), red T
 U
 → typ e
 t
 T
 → typ e
 t
 U
.




Lemma
 typ_conv_conv_coerce : ∀ e
 u
 (U
 : term) v
 (V
 : term), 

  e
 |-- u
 : U
 → e
 |-- v
 : V
 → conv u
 v
 → 

  (U
 = V
 ∨ ∃ s
, e
 |-- U
 >> V
 : s
).