lemma rex_inv_frees (R):
∀L1,L2,T. L1 ⪤[R,T] L2 →
- â\88\80f. L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f → L1 ⪤[cext2 R,cfull,f] L2.
+ â\88\80f. L1 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f → L1 ⪤[cext2 R,cfull,f] L2.
#R #L1 #L2 #T * /3 width=6 by frees_mono, sex_eq_repl_back/
qed-.