/3 width=3 by rexs_step_dx, rex_pair_refl, inj/
qed.
-lemma rexs_tc: â\88\80R,L1,L2,T,f. ð\9d\90\88â\9dªfâ\9d« → TC … (sex cfull (cext2 R) f) L1 L2 →
+lemma rexs_tc: â\88\80R,L1,L2,T,f. ð\9d\90\88â\9d¨fâ\9d© → TC … (sex cfull (cext2 R) f) L1 L2 →
L1 ⪤*[R,T] L2.
#R #L1 #L2 #T #f #Hf #H elim H -L2
[ elim (frees_total L1 T) | #L elim (frees_total L T) ]
-/5 width=7 by sex_sdj, rexs_step_dx, sdj_isid_sn, inj, ex2_intro/
+/5 width=7 by sex_sdj, rexs_step_dx, pr_sdj_isi_sn, inj, ex2_intro/
qed.
(* Advanced eliminators *****************************************************)