X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_structure_inner.ma;h=4de1097bb0b9662c6c76d3d30912cb3cf81849af;hp=99ed6a323f59a60e7cba2473b40d4e270ed2aca5;hb=797a607af83f82102033270087722a7e59ddcd17;hpb=b0c6bbd5db69489a5ebd1b36de6685fa6de441b3

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 99ed6a323..4de1097bb 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
@@ -23,8 +23,9 @@ lemma structure_pic (p):
       ⊗p ϵ 𝐈.
 #p elim p -p
 [ <structure_empty //
-| * [ #k ] #p #IH
+| * [ #k | #k #d ] #p #IH
   [ <structure_d_dx //
+  | <structure_d2_dx //
   | <structure_m_dx //
   | <structure_L_dx //
   | <structure_A_dx //