update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_basic_after.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma
index 788d8c24f5e0365071dc58bda78a068751501c19..b685d17f66ecfff8b1bb38c67a8f251e0ea0175e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma
@@ -20,7 +20,7 @@ include "ground_2/relocation/rtmap_basic.ma".
 (* Properties with composition **********************************************)
 
 lemma after_basic_rc (m2,m1,n2,n1):
-                     m1 â\89¤ m2 â\86\92 m2 â\89¤ m1+n1 â\86\92 ð\9d\90\81â\9d´m2,n2â\9dµ â\8a\9a ð\9d\90\81â\9d´m1,n1â\9dµ â\89\98 ð\9d\90\81â\9d´m1,n2+n1â\9dµ.
+                     m1 â\89¤ m2 â\86\92 m2 â\89¤ m1+n1 â\86\92 ð\9d\90\81â\9d¨m2,n2â\9d© â\8a\9a ð\9d\90\81â\9d¨m1,n1â\9d© â\89\98 ð\9d\90\81â\9d¨m1,n2+n1â\9d©.
 #m2 elim m2 -m2
 [ #m1 #n2 #n1 #Hm21 #_
   <(le_n_O_to_eq … Hm21) -m1 //