(* Advanced properties ******************************************************)
lemma llpx_cpx_conf: ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx h g G 0).
-/3 width=10 by llpx_sn_cpx_conf, cpx_inv_lift1, cpx_lift/ qed-.
+/3 width=10 by cpx_llpx_sn_conf, cpx_inv_lift1, cpx_lift/ qed-.
(* Inversion lemmas on relocation *******************************************)