- #f2V #f2T #HV #HT #Hf2 @(sor_mono … Hf1) -Hf1
- /5 width=3 by sor_eq_repl_fwd2, sor_eq_repl_fwd1, tl_eq_repl/ (**) (* full auto too slow *)
+ #f2V #f2T #HV #HT #Hf2 @(pr_sor_mono … Hf1) -Hf1
+ /5 width=3 by pr_sor_eq_repl_fwd_dx, pr_sor_eq_repl_fwd_sn, pr_tl_eq_repl/ (**) (* full auto too slow *)