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=874cacec64d0aab52ab1a21aad23208f52f50caf;hp=20e372bb652c963e714429752bdedea5816a2c37;hpb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;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/