X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsh_lt.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsh_lt.ma;h=d33515ef80dfb47e04a986bcdf781b1a77e1ebf3;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=b7e10f851883233aae42c87faa1966256653c025;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
index b7e10f851..d33515ef8 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
@@ -91,7 +91,7 @@ elim (lt_or_ge s2 s1) #Hs
     | /3 width=2 by ex_intro, or_introl/
     ]
   | -IH @or_introl @(ex_intro … 1) // (**) (* auto fails *)
-  | lapply (transitive_lt s1 ??? Hs21) [ /2 width=1 by next_lt/ ] -Hs12 #Hs12 
+  | lapply (transitive_lt s1 ??? Hs21) [ /2 width=1 by next_lt/ ] -Hs12 #Hs12
     elim (IH (s2-⫯[h]s1)) -IH
     [3: /3 width=1 by next_lt, monotonic_lt_minus_r/ ]
     >minus_minus_m_m [2,4: /2 width=1 by lt_to_le/ ] -Hs21