X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrop_sfr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrop_sfr.ma;h=83c157a5af97bbc90e0830d30089cc2377da67eb;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=4f4060ff166b641583c1f963fd8551f577d0bbc4;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
index 4f4060ff1..83c157a5a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
@@ -55,7 +55,7 @@ lemma sfr_ldrop: ∀L,d,e.
   #e #_ #H0
   >(H0 I L V 0 ? ? ?) //
   /5 width=6 by sfr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
-| #d #_ #e #H0 
+| #d #_ #e #H0
   /5 width=6 by sfr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
 ]
 qed.