-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+lapply (pr_tl_eq_repl … H2) -H2 #H2
+lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy
+lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (pr_sle_inv_tl_sn … Hfg) -Hfg #Hfg