- acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
- ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 ⊑[RP] L0 →
- ⦃L2, T0⦄ ϵ[RP] 〚A〛.
-#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
-[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
+ acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
+ ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⊑[RP] L0 →
+ ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
+#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
+[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20