-theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
- gcp RR RS RP → gcr RR RS RP RP →
- ∀G,L1,T,A. ⦃G,L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
- ∀T0. ⇧*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
- ⦃G,L2,T0⦄ ϵ[RP] 〚A〛.
+theorem acr_aaa_lsubc_lifts (RR) (RS) (RP):
+ gcp RR RS RP → gcr RR RS RP RP →
+ ∀G,L1,T,A. ❪G,L1❫ ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
+ ∀T0. ⇧*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+ ❪G,L2,T0❫ ϵ ⟦A⟧[RP].