X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_structure_inner.ma;h=99ed6a323f59a60e7cba2473b40d4e270ed2aca5;hb=9e31ac1f3f868349154b0ce2e550e2476aaf6a30;hp=5c0e5e6eb549a76a91567b1ee9a801976be46b02;hpb=8a47ade5ffd1942f9d16474c547e5050caab3cc8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
index 5c0e5e6eb..99ed6a323 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
@@ -21,9 +21,9 @@ include "delayed_updating/syntax/path_inner.ma".
 
 lemma structure_pic (p):
       ⊗p ϵ 𝐈.
-#p @(list_ind_rcons … p) -p
+#p elim p -p
 [ <structure_empty //
-| #p * [ #n ] #IH
+| * [ #k ] #p #IH
   [ <structure_d_dx //
   | <structure_m_dx //
   | <structure_L_dx //