X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Fdsubst.ma;h=c43cd1d740601d11154e34beb0e754c34f8628fd;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=20e372bb652c963e714429752bdedea5816a2c37;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma
index 20e372bb6..c43cd1d74 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma
@@ -41,7 +41,7 @@ theorem fdsubst_delift: ∀K,V,T,L,d.
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
   [ -HLK >(tri_lt ?????? Hid) /3 width=3/
-  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *)   
+  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *)
   | -HLK >(tri_gt ?????? Hid) /3 width=3/
   ]
 | * /3 width=1/ /4 width=1/