update in delayed_updating and ground

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind2_rmap_unprotected.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
index 1f2a9d530ba64c14e03bfa4531381e49789804ed..b8cb1d2cf7cb176180bf3e5d16b24a6801097b86 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
@@ -30,8 +30,8 @@ lemma b_balanced: ⊗b ϵ 𝐁.
 /2 width=1 by pbc_empty, pbc_redex/
 qed.
 
-lemma b_closed: b ϵ 𝐂❨𝟎❩.
-/4 width=1 by pcc_A_sn, pcc_empty, pcc_d_dx, pcc_L_dx/
+lemma b_closed: b ϵ 𝐂❨Ⓕ,𝟎❩.
+/4 width=1 by pcc_A_sn, pcc_empty, pcc_false_d_dx, pcc_L_dx/
 qed.
 
 lemma b_unwind2_rmap_unfold (f):