X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind_gen_structure.ma;h=d8a44810cf3a92f9619a5fba295da00e234ea933;hb=ad6182251b8192ee7d25c53156afbce35e3715b6;hp=fcc04282bc21718c428a2716f8f4079d004c188d;hpb=77479649510792efe4d9cbff508e118360862594;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
index fcc04282b..d8a44810c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -73,29 +73,29 @@ qed-.
 
 (* Advanced constructions with list_rcons ***********************************)
 
-lemma unwind_gen_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱((f n)＠⧣❨n❩) = ◆[f](p◖𝗱n).
-#n #p #f <unwind_gen_append_proper_dx // 
+lemma unwind_gen_d_dx (f) (p) (n):
+      (⊗p)◖𝗱(f＠⧣❨n❩) = ◆[f](p◖𝗱n).
+#f #p #n <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_m_dx (p) (f):
+lemma unwind_gen_m_dx (f) (p):
       ⊗p = ◆[f](p◖𝗺).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_L_dx (p) (f):
+lemma unwind_gen_L_dx (f) (p):
       (⊗p)◖𝗟 = ◆[f](p◖𝗟).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_A_dx (p) (f):
+lemma unwind_gen_A_dx (f) (p):
       (⊗p)◖𝗔 = ◆[f](p◖𝗔).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_S_dx (p) (f):
+lemma unwind_gen_S_dx (f) (p):
       (⊗p)◖𝗦 = ◆[f](p◖𝗦).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
 lemma unwind_gen_root (f) (p):
@@ -110,7 +110,7 @@ qed-.
 
 lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
       (𝗱k◗q) = ◆[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & (f h)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+      ∃∃r,h. 𝐞 = ⊗r & f＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
 #k #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_gen_empty #H destruct