-lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
- ∀des,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L →
- all … (RP L) Vs → all … (RP L0) V0s.
-#RR #RS #RP #HRP #des #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //
+lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
+ ∀des,G,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L →
+ all … (RP G L) Vs → all … (RP G L0) V0s.
+#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //