- lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
- lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
- lapply (sor_comm … Hz) -Hz #Hz
- lapply (sor_mono … f Hz ?) // -Hz #H
- lapply (sor_inv_sle_sn … Hf) -Hf #Hf
- lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0
+ lapply (pr_sor_eq_repl_back_sn … Hz … H02) -g0 #Hz
+ lapply (pr_sor_eq_repl_back_dx … Hz … H1) -z1 #Hz
+ lapply (pr_sor_comm … Hz) -Hz #Hz
+ lapply (pr_sor_mono … f Hz ?) // -Hz #H
+ lapply (pr_sor_inv_sle_sn … Hf) -Hf #Hf
+ lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by pr_eq_next/ -z #Hf0