update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / lsubf_lsubf.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma
index 63173fbf7f0feaa436d7991a30de304928b1e61c..7d162a58ed9fdc7c84dffe124c4e4c353de6fdd3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma
@@ -20,9 +20,9 @@ include "static_2/static/lsubf.ma".
 (* Main properties **********************************************************)
 
 theorem lsubf_sor:
-        â\88\80K,L,g1,f1. â¦\83K,g1â¦\84 â«\83ð\9d\90\85+ â¦\83L,f1â¦\84 →
-        â\88\80g2,f2. â¦\83K,g2â¦\84 â«\83ð\9d\90\85+ â¦\83L,f2â¦\84 →
-        â\88\80g. g1 â\8b\93 g2 â\89\98 g â\86\92 â\88\80f. f1 â\8b\93 f2 â\89\98 f â\86\92 â¦\83K,gâ¦\84 â«\83ð\9d\90\85+ â¦\83L,fâ¦\84.
+        â\88\80K,L,g1,f1. â\9dªK,g1â\9d« â«\83ð\9d\90\85+ â\9dªL,f1â\9d« →
+        â\88\80g2,f2. â\9dªK,g2â\9d« â«\83ð\9d\90\85+ â\9dªL,f2â\9d« →
+        â\88\80g. g1 â\8b\93 g2 â\89\98 g â\86\92 â\88\80f. f1 â\8b\93 f2 â\89\98 f â\86\92 â\9dªK,gâ\9d« â«\83ð\9d\90\85+ â\9dªL,fâ\9d«.
 #K elim K -K
 [ #L #g1 #f1 #H1 #g2 #f2 #H2 #g #Hg #f #Hf
   elim (lsubf_inv_atom1 … H1) -H1 #H1 #H destruct