X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;h=a769327f65b218f655530102b435ca614b60eb22;hp=2e638b8ac43bfba05ccc9783d2045d130d302a9d;hb=9e31ac1f3f868349154b0ce2e550e2476aaf6a30;hpb=797a607af83f82102033270087722a7e59ddcd17

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index 2e638b8ac..a769327f6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -23,12 +23,11 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
-  [ label_d k    ⇒ depth q
-  | label_d2 k d ⇒ depth q
-  | label_m      ⇒ depth q
-  | label_L      ⇒ ↑(depth q)
-  | label_A      ⇒ depth q
-  | label_S      ⇒ depth q
+  [ label_d k ⇒ depth q
+  | label_m   ⇒ depth q
+  | label_L   ⇒ ↑(depth q)
+  | label_A   ⇒ depth q
+  | label_S   ⇒ depth q
   ]
 ].
 
@@ -45,10 +44,6 @@ lemma depth_d_dx (p) (k):
       ♭p = ♭(p◖𝗱k).
 // qed.
 
-lemma depth_d2_dx (p) (k) (d):
-      ♭p = ♭(p◖𝗱❨k,d❩).
-// qed.
-
 lemma depth_m_dx (p):
       ♭p = ♭(p◖𝗺).
 // qed.
@@ -70,9 +65,8 @@ lemma depth_S_dx (p):
 theorem depth_append (p) (q):
         (♭p)+(♭q) = ♭(p●q).
 #p #q elim q -q //
-* [ #k | #k #d ] #q #IH <list_append_lcons_sn
+* [ #k ] #q #IH <list_append_lcons_sn
 [ <depth_d_dx <depth_d_dx //
-| <depth_d2_dx <depth_d2_dx //
 | <depth_m_dx <depth_m_dx //
 | <depth_L_dx <depth_L_dx //
 | <depth_A_dx <depth_A_dx //
@@ -86,10 +80,6 @@ lemma depth_d_sn (p) (k):
       ♭p = ♭(𝗱k◗p).
 // qed.
 
-lemma depth_d2_sn (p) (k) (d):
-      ♭p = ♭(𝗱❨k,d❩◗p).
-// qed.
-
 lemma depth_m_sn (p):
       ♭p = ♭(𝗺◗p).
 // qed.