update in delayed_updating

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

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 25678301b5951bb84b6edaf188cbf9d2f05ebbc5..b2b0cb03f9e6b681b1ab78ede143d96e27a8b42d 100644 (file)
--- 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):