Library Lambda.TPOSR.SubstitutionTPOSR


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.PreCtxCoercion.

Require
 Import
 Lambda.TPOSR.LeftReflexivity.

Require
 Import
 Lambda.TPOSR.PreSubstitutionTPOSR.

Require
 Import
 Lambda.TPOSR.RightReflexivity.







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.




Corollary
 substitution_tposr_tposr_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 ->

   ∀ e
 u
 v
 U
, e
 |-- u
 -> v
 : U
 ->

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) -> (lsubst_rec d'
 v
 n
) : (lsubst_rec d
 U
 n
).




Corollary
 substitution_tposr_tposr_wf_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> 

   ∀ e
, tposr_wf e
 -> ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> 

   trunc _
 n
 f
 g
 -> tposr_wf f
.




Corollary
 substitution_tposr_eq_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 ->

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

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) ~= (lsubst_rec d'
 v
 n
) : s
.




Corollary
 substitution_tposr_coerce_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> 

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

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) >-> (lsubst_rec d'
 v
 n
) : s
.




Corollary
 substitution_tposr_tposr : ∀ e
 t
 u
 v
 U
, (t
 :: e
) |-- u
 -> v
 : U
 ->

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- (lsubst d
 u
) -> (lsubst d'
 v
) : (lsubst d
 U
).




Corollary
 substitution_tposr_eq : 

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

   ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> 

   e
 |-- (lsubst d
 u
) ~= (lsubst d'
 v
) : s
.




Corollary
 substitution_tposr_coerce : 

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

   ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> 

   e
 |-- (lsubst d
 u
) >-> (lsubst d'
 v
) : s
.




Corollary
 substitution_tposr_tposrp_aux : ∀ G
 u
 v
 U
, G
 |-- u
 -+> v
 : U
 -> ∀ t
 e
, G
 = (t
 :: e
) ->

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> 

  e
 |-- (lsubst d
 u
) -+> (lsubst d'
 v
) : (lsubst d
 U
).




Corollary
 substitution_tposr_tposrp : ∀ t
 e
 u
 v
 U
, t
 :: e
 |-- u
 -+> v
 : U
 -> 

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> 

 e
 |-- (lsubst d
 u
) -+> (lsubst d'
 v
) : (lsubst d
 U
).




Corollary
 substitution_sorted_n : 

  ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> 

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

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) -> (lsubst_rec d'
 v
 n
) : Srt_l s
.




Corollary
 substitution_sorted : ∀ e
 t
 u
 v
 s
, (t
 :: e
) |-- u
 -> v
 : Srt_l s
 ->

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- (lsubst d
 u
) -> (lsubst d'
 v
) : Srt_l s
.




Hint
 Resolve
 substitution_tposr_tposr substitution_tposr_coerce substitution_tposr_eq substitution_tposr_tposrp : ecoc
.