X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind_gen_after.ma;h=2954be831ebeb65a4e3b5da04fd6411575e7d196;hb=ad6182251b8192ee7d25c53156afbce35e3715b6;hp=9d4955ff9be28ed5272e8a66c862c42a2fafa1d8;hpb=9b4e20442ec5a4028cfe2b6fe836c94acdb033b8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
index 9d4955ff9..2954be831 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
@@ -20,7 +20,6 @@ include "ground/relocation/tr_compose_pap.ma".
 (* Properties with tr_compose ***********************************************)
 
 lemma unwind_gen_after (f2) (f1) (p):
-      ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)@❨n❩))∘(f1 n)]p.
+      ◆[f2]◆[f1]p = ◆[f2∘f1]p.
 #f2 #f1 #p @(path_ind_unwind … p) -p //
-#n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
 qed.