Library Lambda.Russell.GenerationNotKind


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.




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
 lift_rec_eq_sort : ∀ t
 n
 k
 s
, lift_rec n
 t
 k
 = Srt s
 → t
 = Srt s
.




Lemma
 lift_eq_sort : ∀ t
 n
 s
, lift n
 t
 = Srt s
 → t
 = Srt s
.




Lemma
 typ_not_kind : ∀ G
 t
 T
, G
 |-- t
 : T
 → t
 ≠ Srt kind.




Lemma
 typ_not_kind2 : ∀ G
 T
, ¬ G
 |-- Srt kind : T
.




Hint
 Resolve
 lift_eq_sort typ_not_kind2 : coc
.




Fixpoint
 type_no_kind (t
 : term) : Prop
 :=

  match
 t
 with


  | Prod U
 V
 ⇒ type_no_kind U
 ∧ type_no_kind V


  | Sum U
 V
 ⇒ type_no_kind U
 ∧ type_no_kind V


  | Srt kind ⇒ False

  | _
 ⇒ True

  end
.




Lemma
 type_has_no_kind : ∀ G
 t
 T
, G
 |-- t
 : T
 → type_no_kind t
.




Lemma
 type_no_kind_not_kind : ∀ t
, type_no_kind t
 → t
 ≠ Srt kind.




Lemma
 lift_type_range_eq_sort : ∀ n
 t
 k
, type_no_kind (lift_rec n
 t
 k
) → 

  type_no_kind t
.




Lemma
 type_no_kind_lift : ∀ n
 t
 k
, type_no_kind t
 →

  type_no_kind (lift_rec n
 t
 k
).




Lemma
 type_range_subst_not_kind : ∀ u
 v
 n
, type_no_kind u
 →

  type_no_kind v
 → type_no_kind (subst_rec u
 v
 n
).




Lemma
 type_no_kind_type : ∀ G
 t
 T
, G
 |-- t
 : T
 → 

  ∀ U
 V
, (T
 = Prod U
 V
 ∨ T
 = Sum U
 V
) → type_no_kind T
.




Lemma
 type_no_kind_prod_type : ∀ G
 t
 U
 V
, 

  G
 |-- t
 : Prod U
 V
 → type_no_kind (Prod U
 V
).




Lemma
 type_no_kind_sum_type : ∀ G
 t
 U
 V
, 

  G
 |-- t
 : Sum U
 V
 → type_no_kind (Sum U
 V
).