partial update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_structure_inner.ma

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 5c0e5e6eb549a76a91567b1ee9a801976be46b02..4de1097bb0b9662c6c76d3d30912cb3cf81849af 100644 (file)
--- 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,10 +21,11 @@ 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 | #k #d ] #p #IH
   [ <structure_d_dx //
+  | <structure_d2_dx //
   | <structure_m_dx //
   | <structure_L_dx //
   | <structure_A_dx //