-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
-elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
+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
+elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2