Library Lambda.TPOSR.Thinning


Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Env.

Require
 Import
 Lambda.TPOSR.Conv.

Require
 Import
 Lambda.TPOSR.Types.

Require
 Import
 Lambda.TPOSR.LeftReflexivity.







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
 ind_thinning : ∀ A
,

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

   ∀ n
 f
, ins_in_lenv A
 n
 e
 f
 -> tposr_wf f
 ->

   f
 |-- (llift_rec 1 u
 n
) -> (llift_rec 1 v
 n
) : (llift_rec 1 T
 n
)) ∧

  (∀ e
, tposr_wf e
 -> True) ∧

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

   ∀ n
 f
, ins_in_lenv A
 n
 e
 f
 -> tposr_wf f
 ->

   f
 |-- (llift_rec 1 u
 n
) ~= (llift_rec 1 v
 n
) : s
) ∧

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

   ∀ n
 f
, ins_in_lenv A
 n
 e
 f
 -> tposr_wf f
 ->

   f
 |-- (llift_rec 1 u
 n
) >-> (llift_rec 1 v
 n
) : s
).




Corollary
 thinning :

   ∀ e
 t
 t'
 T
,

   e
 |-- t
 -> t'
 : T
 -> ∀ A
, tposr_wf (A
 :: e
) -> (A
 :: e
) |-- llift 1 t
 -> llift 1 t'
 : (llift 1 T
).




Corollary
 thinning_eq :

   ∀ e
 t
 t'
 s
,

   e
 |-- t
 ~= t'
 : s
 -> 

   ∀ A
, tposr_wf (A
 :: e
) -> (A
 :: e
) |-- (llift 1 t
) ~= llift 1 t'
 : s
.




Corollary
 thinning_coerce :

   ∀ e
 t
 t'
 s
,

   e
 |-- t
 >-> t'
 : s
 -> 

   ∀ A
, tposr_wf (A
 :: e
) -> (A
 :: e
) |-- (llift 1 t
) >-> llift 1 t'
 : s
.




Lemma
 thinning_n :

   ∀ n
 e
 f
,

   trunc _
 n
 e
 f
 ->

   ∀ t
 t'
 T
, f
 |-- t
 -> t'
 : T
 -> tposr_wf e
 -> e
 |-- (llift n
 t
) -> (llift n
 t'
) : (llift n
 T
).




Lemma
 thinning_n_eq :

   ∀ n
 e
 f
,

   trunc _
 n
 e
 f
 ->

   ∀ t
 t'
 s
, f
 |-- t
 ~= t'
 : s
 -> tposr_wf e
 -> e
 |-- (llift n
 t
) ~= (llift n
 t'
) : s
.




Lemma
 thinning_n_coerce :

   ∀ n
 e
 f
,

   trunc _
 n
 e
 f
 ->

   ∀ t
 t'
 s
, f
 |-- t
 >-> t'
 : s
 -> tposr_wf e
 -> e
 |-- (llift n
 t
) >-> (llift n
 t'
) : s
.




Lemma
 wf_sort_lift :

 ∀ n
 e
 t
, tposr_wf e
 -> item_llift t
 e
 n
 -> ∃ s
 : sort, e
 |-- t
 -> t
 : (Srt_l s
).




Hint
 Resolve
 thinning thinning_eq thinning_coerce thinning_n : coc
.