partial commit in delayed_updating

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

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 a9b2683b66e2f83105c57254279fdf1beaaf140d..2954be831ebeb65a4e3b5da04fd6411575e7d196 100644 (file)
--- 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.