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 f0ffe995bc1d35c255cc2f3e459745d6a01ada6a..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