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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
index 112a98c39..ca1375558 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
@@ -65,7 +65,7 @@ lemma ibfr_appl_sd (v1) (v2) (t) (r):
 qed.
 
 lemma ibfr_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
@@ -82,7 +82,7 @@ lemma ibfr_beta_0 (v) (t) (q) (n):
 qed.
 
 lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
-      q Ïµ ðâ¨â»,nâ© â qâð±ân Ïµ t â
+      q Ïµ ðâ¨â»,n,ðâ© â qâð±ân Ïµ t â
       ï¼ v.ï¼ v1.ð.ð.t â¡ð¢ðð[ðâðâðâðâq] ï¼ v.ï¼ v1.ð.ð.(t[âqâð ¡[ð®â¨âânâ©]v]).
 #v #v1 #t #q #n #Hn #Ht
 @(ex6_5_intro â¦ (ð) (ðâðâð) q (ð) â¦ Hn) -Hn