update in ground static_2 basic_2 apps_2

[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 8ad9f517d929336cd921b0fe86e8f7fe0801563c..f4d632339b8f0c573f9c33b05ace4cd62df02b90 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. â\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«.
+        â\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