X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_structure.ma;h=288575c4e7680630668be3a61108478261a6d0c4;hb=9e31ac1f3f868349154b0ce2e550e2476aaf6a30;hp=3b91954fd83ca4a90115038959bdd2dc718f778d;hpb=61bc42e04598a9f5e489c3867af72e700c7fda04;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 3b91954fd..288575c4e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -65,20 +65,22 @@ lemma structure_S_dx (p):
 
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
-#p elim p -p [| * [ #k ] #p #IH ] //
+#p elim p -p //
+* [ #k ] #p #IH //
 qed.
 
 theorem structure_append (p) (q):
         ⊗p●⊗q = ⊗(p●q).
-#p #q elim q -q [| * [ #k ] #q #IH ]
-[||*: <list_append_lcons_sn ] //
+#p #q elim q -q //
+* [ #k ] #q #IH //
+<list_append_lcons_sn //
 qed.
 
 (* Constructions with path_lcons ********************************************)
 
 lemma structure_d_sn (p) (k):
       ⊗p = ⊗(𝗱k◗p).
-#p #n <structure_append //
+#p #k <structure_append //
 qed.
 
 lemma structure_m_sn (p):