Library Lambda.CCSum.Unicity


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.CCSum.Types.

Require
 Import
 Lambda.CCSum.Inversion.

Require
 Import
 Lambda.CCSum.Thinning.

Require
 Import
 Lambda.CCSum.Substitution.

Require
 Import
 Lambda.CCSum.TypeCase.

Require
 Import
 Lambda.CCSum.SubjectReduction.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




  Theorem
 typ_unique :

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




  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 :

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

   typ e
 u
 U
 → typ e
 v
 V
 → conv u
 v
 → conv U
 V
.