renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lsubf_lsubr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubr.ma
index 936518fcbbf7e54683332f8854f91bcc7701c74c..24b7e90d2b63667ebf0038a1bec6e9f099c9f6fc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubr.ma
@@ -44,8 +44,8 @@ elim (isid_inv_gen … Hf2) -Hf2 #g2 #Hg2 #H destruct
 /3 width=1 by lsubf_push/
 qed.
 
-lemma lsubr_lsubf: â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 → ∀L1. L1 ⫃ L2 →
-                   â\88\80f1. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f1 → ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄.
+lemma lsubr_lsubf: â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 → ∀L1. L1 ⫃ L2 →
+                   â\88\80f1. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f1 → ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄.
 #f2 #L2 #T #H elim H -f2 -L2 -T
 [ #f2 #L2 #s #Hf2 #L1 #HL12 #f1 #Hf1
   lapply (frees_inv_sort … Hf1) -Hf1 /2 width=1 by lsubr_lsubf_isid/