X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_unprotected.ma;h=b8cb1d2cf7cb176180bf3e5d16b24a6801097b86;hp=1f2a9d530ba64c14e03bfa4531381e49789804ed;hb=d06053844638d88936d711b66fddbcca2a9add1c;hpb=9e31ac1f3f868349154b0ce2e550e2476aaf6a30 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 1f2a9d530..b8cb1d2cf 100644 --- 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):