-elim (sor_isfin_ex f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-/4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
+elim (pr_sor_isf_bi f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #f #Hf #_
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
+/4 width=15 by frees_bind_void, frees_bind, pr_sor_monotonic_sle, pr_sle_tl, ex4_4_intro/