Library Lambda.Meta.TPOSR_JRussell


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.Tactics.




Require
 Import
 Lambda.JRussell.Types.

Require
 Import
 Lambda.JRussell.Basic.

Require
 Import
 Lambda.JRussell.Coercion.

Require
 Import
 Lambda.JRussell.Generation.

Require
 Import
 Lambda.JRussell.Thinning.

Require
 Import
 Lambda.JRussell.Substitution.

Require
 Import
 Lambda.JRussell.Validity.

Require
 Import
 Lambda.JRussell.UnicityOfSorting.




Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.Conv.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Env.

Require
 Import
 Lambda.TPOSR.Types.

Require
 Import
 Lambda.TPOSR.Unlab.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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

Implicit
 Types
 e
 f
 g
 : lenv.







Lemma
 item_unlab : ∀ n
 t
 e
, item lterm t
 e
 n
 -> item term (|t|) (unlab_ctx e
) n
.




Theorem
 unlab_sound  : 

  (∀ e
 u
 v
 T
, e
 |-- u
 -> v
 : T
 -> 

  (unlab_ctx e
) |-= (|u|) = (|v|) : (|T|)) ∧

  (∀ e
, tposr_wf e
 -> 

  (unlab_ctx e
) |-= Srt prop : Srt kind ∧

  (unlab_ctx e
) |-= Srt set : Srt kind ∧

  (∀ A
 n
, item_llift A
 e
 n
 -> 

  (unlab_ctx e
) |-= Ref n
 : (|A|))) ∧

  (∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 ->

  (unlab_ctx e
) |-= (|u|) = (|v|) : Srt s
) ∧

  (∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 ->

  (unlab_ctx e
) |-= (|u|) >> (|v|) : s
).




Corollary
 unlab_sound_type : ∀ e
 u
 v
 T
, e
 |-- u
 -> v
 : T
 -> 

  (unlab_ctx e
) |-= (|u|) = (|v|) : (|T|).




Corollary
 unlab_sound_tposrp : ∀ e
 u
 v
 T
, e
 |-- u
 -+> v
 : T
 -> 

  (unlab_ctx e
) |-= (|u|) = (|v|) : (|T|).




Corollary
 unlab_sound_wf :

  (∀ e
, tposr_wf e
 -> 

  (unlab_ctx e
) |-= Srt prop : Srt kind ∧

  (unlab_ctx e
) |-= Srt set : Srt kind ∧

  (∀ A
 n
, item_llift A
 e
 n
 -> 

  (unlab_ctx e
) |-= Ref n
 : (|A|))).




Corollary
 unlab_sound_eq : ∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 -> 

  (unlab_ctx e
) |-= (|u|) = (|v|) : Srt s
.




Corollary
 unlab_sound_coerce : ∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 -> 

  (unlab_ctx e
) |-= (|u|) >> (|v|) : s
.




Theorem
 tposr_unique_sort : ∀ G
 A
 B
 C
 s
 s'
, G
 |-- A
 -> B
 : Srt_l s
 -> G
 |-- A
 -> C
 : Srt_l s'
 ->

  s
 = s'
.




Theorem
 tposr_eq_unique_sort : ∀ G
 A
 B
 C
 s
 s'
, G
 |-- A
 ~= B
 : s
 -> G
 |-- A
 ~= C
 : s'
 ->

  s
 = s'
.




Theorem
 tposr_coerce_unique_sort : ∀ G
 A
 B
 C
 s
 s'
, G
 |-- A
 >-> B
 : s
 -> G
 |-- A
 >-> C
 : s'
 ->

  s
 = s'
.