(* Relocation properties ****************************************************)
lemma cpds_lift: ∀h,g,G. l_liftable (cpds h g G).
(* Relocation properties ****************************************************)
lemma cpds_lift: ∀h,g,G. l_liftable (cpds h g G).
-/3 width=15 by cprs_lift, da_lift, lsstas_lift, ex4_3_intro/
+/3 width=16 by cprs_lift, da_lift, lsstas_lift, ex4_3_intro/
lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1
elim (lsstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1
elim (lsstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1