lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
∀des,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 →
RP L V → RP L0 V0.
lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
∀des,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 →
RP L V → RP L0 V0.