@@ -18,7+18,7 @@ include "basic_2/static/frees.ma".
(* Main inversion lemmas ****************************************************)
(* Main inversion lemmas ****************************************************)
-theorem frees_mono: â\88\80f1,L,T. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f1 â\86\92 â\88\80f2. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 â\86\92 f1 â\89\97 f2.
+theorem frees_mono: â\88\80f1,L,T. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f1 â\86\92 â\88\80f2. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 â\86\92 f1 â\89¡ f2.