(* Advanced inversion lemmas ************************************************)
lemma lfxs_inv_frees: ∀R,L1,L2,T. L1 ⪤*[R, T] L2 →
- â\88\80f. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f → L1 ⪤*[cext2 R, cfull, f] L2.
+ â\88\80f. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f → L1 ⪤*[cext2 R, cfull, f] L2.
#R #L1 #L2 #T * /3 width=6 by frees_mono, lexs_eq_repl_back/
qed-.