update in ground

[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 9d4955ff9be28ed5272e8a66c862c42a2fafa1d8..a9b2683b66e2f83105c57254279fdf1beaaf140d 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,7 @@ 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 = ◆[λn.(f2 ((f1 n)＠⧣❨n❩))∘(f1 n)]p.
 #f2 #f1 #p @(path_ind_unwind … p) -p //
 #n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
 qed.