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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
index 25678301b..b2b0cb03f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -39,12 +39,6 @@ lemma pic_inv_d_dx (p) (k):
 #q * -q [|*: #q ] #H0 destruct
 qed-.
 
-lemma pic_inv_d2_dx (p) (k) (d):
-      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
-#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
-#q * -q [|*: #q ] #H0 destruct
-qed-.
-
 (* Constructions with path_lcons ********************************************)
 
 lemma pic_m_sn (p):