-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 //
-#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s
-@conj /2 width=1/ /2 width=6 by rp_lifts/
+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 //
+#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * /3 width=6 by rp_lifts, conj/