-lemma gcp2_lifts_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. l_liftables1_all (RP G) (Ⓕ).
-#RR #RS #RP #H #G @l1_liftables_liftables_all /2 width=7 by gcp2_lifts/
+lemma gcp2_lifts_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftables1_all (RP G) (Ⓕ).
+#RR #RS #RP #H #G @d1_liftables_liftables_all /2 width=7 by gcp2_lifts/