X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fprototerm_eq.ma;h=5604578e52fa9839edb1a6ae9c6caf44344f5ebe;hp=baffe070a138b076ffa0a3965cc98ba7379543b8;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hpb=48cd63fc7f4415925582eae224a36a9c1bb3cc06

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
index baffe070a..5604578e5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
@@ -17,6 +17,13 @@ include "ground/lib/subset_equivalence.ma".
 
 (* EQUIVALENCE FOR PROTOTERM ************************************************)
 
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_empty_dx (t):
+      t ⇔ t⋔𝐞.
+/2 width=1 by conj/
+qed.
+
 (* Constructions with prototerm_root ****************************************)
 
 lemma prototerm_root_incl_repl: