update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / dbfr_constructors.ma

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 4dd861087c868dae551e926f0ff2e4032f419432..5225ef5378459c5bf1583ba1e7436606743fd98a 100644 (file)
--- 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
@@ -82,7 +82,7 @@ qed.
 (*
 lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
       q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
-      ï¼ v.ï¼ v1.ð\9d\9b\8c.ð\9d\9b\8c.t â\9e¡ð\9d\90\9dð\9d\90\9bð\9d\90\9f[ð\9d\97\94â\97\97ð\9d\97\94â\97\97ð\9d\97\9fâ\97\97ð\9d\97\9fâ\97\97q] ï¼ v.ï¼ v1.ð\9d\9b\8c.ð\9d\9b\8c.(t[â\8b\94qâ\86\90ð\9f ¡[ð\9d\90®â\9d¨â\86\91â\86\91nâ\9d©]v]).
+      ï¼ v.ï¼ v1.ð\9d\9b\8c.ð\9d\9b\8c.t â\9e¡ð\9d\90\9dð\9d\90\9bð\9d\90\9f[ð\9d\97\94â\97\97ð\9d\97\94â\97\97ð\9d\97\9fâ\97\97ð\9d\97\9fâ\97\97q] ï¼ v.ï¼ v1.ð\9d\9b\8c.ð\9d\9b\8c.(t[â\8b\94qâ\86\90ð\9d\9b\95â\86\91â\86\91n.v]).
 #v #v1 #t #q #n #Hn #Ht
 @(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
 [ //