λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / sh_lt.ma

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 b7e10f851883233aae42c87faa1966256653c025..d33515ef80dfb47e04a986bcdf781b1a77e1ebf3 100644 (file)
--- 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