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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
index 30a2770e2..be3b82e04 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
@@ -30,12 +30,18 @@ interpretation
   'Pitchfork t p = (prototerm_grafted p t).
 
 definition prototerm_root: prototerm → prototerm ≝
-           λt,q. ∃r. q●r ϵ t.
+           λt,q. ∃r. r ϵ t⋔q.
 
 interpretation
   "root (prototerm)"
   'UpTriangle t = (prototerm_root t).
 
+(* Basic inversions *********************************************************)
+
+lemma prototerm_grafted_inv_gen (t) (p) (q):
+      q ϵ t⋔p → p●q ϵ t.
+// qed-.
+
 (* Basic constructions ******************************************************)
 
 lemma prototerm_in_comp_root (p) (t):