X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fdbfr_constructors.ma;h=5225ef5378459c5bf1583ba1e7436606743fd98a;hb=ea71486fd1aab2eae2bab42729a66ae775c7f248;hp=f0ffe995bc1d35c255cc2f3e459745d6a01ada6a;hpb=73cc0c523c5264f2883c25f6735be325e5cfd1da;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
index f0ffe995b..5225ef537 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
@@ -64,7 +64,7 @@ lemma dbfr_appl_sd (v1) (v2) (t) (r):
 qed.
 
 lemma dbfr_beta_0 (v) (t) (q) (n):
-      q Ïµ ðâ¨â»,nâ© â qâð±ân Ïµ t â
+      q Ïµ ðâ¨â»,n,ðâ© â qâð±ân Ïµ t â
       ï¼ v.ð.t â¡ððð[ðâðâq] ï¼ v.ð.(t[âqâðân.v]).
 #v #t #q #n #Hn #Ht
 @(ex6_5_intro â¦ (ð) (ð) q (ð) â¦ Hn) -Hn