| /3 width=7 by ldrops_cons, lifts_cons/
]
qed.
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
| /3 width=7 by ldrops_cons, lifts_cons/
]
qed.
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (