X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind1%2Funwind.ma;h=e5a6ea13f100fee50a70a3d77c110baffafcb45d;hb=3c78efa39d4783f83638b1aabe8d776d83aabf35;hp=43e634114db60fd29c22830f179bbef666cd96b1;hpb=d08b01eee540a6e955cb12cb7421da4198a4ef48;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
index 43e634114..e5a6ea13f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
@@ -63,11 +63,11 @@ lemma unwind_empty (A) (k) (f):
       k f (𝐞) = ▼{A}❨k, f, 𝐞❩.
 // qed.
 
-lemma unwind_d_empty_sn (A) (k) (n) (f):
+lemma unwind_d_empty (A) (k) (n) (f):
       ▼❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐮❨f@❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
 // qed.
 
-lemma unwind_d_lcons_sn (A) (k) (p) (l) (n) (f):
+lemma unwind_d_lcons (A) (k) (p) (l) (n) (f):
       ▼❨k, 𝐮❨f@❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
 // qed.
 
@@ -93,11 +93,11 @@ lemma unwind_path_empty (f):
       (𝐞) = ▼[f]𝐞.
 // qed.
 
-lemma unwind_path_d_empty_sn (f) (n):
+lemma unwind_path_d_empty (f) (n):
       𝗱(f@❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
 // qed.
 
-lemma unwind_path_d_lcons_sn (f) (p) (l) (n):
+lemma unwind_path_d_lcons (f) (p) (l) (n):
       ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
 // qed.