Library Lambda.JRussell.Basic


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.JRussell.Types.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




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




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




Lemma
 coerce_prop_prop : nil |-= Srt prop >> Srt prop : kind.




Lemma
 coerce_set_set : nil |-= Srt set >> Srt set : kind.




Lemma
 coerce_is_prop : ∀ s
, is_prop s
 → nil |-= Srt s
 >> Srt s
 : kind.




Lemma
 consistency_ind :

  (∀ e
 t
 T
, e
 |-= t
 : T
 → consistent e
) ∧

  (∀ e
 T
 U
 s
, e
 |-= T
 >> U
 : s
 → consistent e
) ∧

  (∀ e
 U
 V
 T
, e
 |-= U
 = V
 : T
 → consistent e
).




Lemma
 typ_consistent : ∀ e
 t
 T
, e
 |-= t
 : T
 → consistent e
.




Lemma
 jeq_consistent : ∀ e
 U
 V
 T
, e
 |-= U
 = V
 : T
 → consistent e
.




Lemma
 coerce_consistent : ∀ e
 T
 U
 s
, e
 |-= T
 >> U
 : s
 → consistent e
.




Hint
 Resolve
 coerce_prop_prop coerce_set_set coerce_is_prop : coc
.

Hint
 Resolve
 lift_sort left_not_kind : coc
.