update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
index 30a2770e279bceb6c3baa14bcd51e0dcc570a789..be3b82e04681beceee9499be156a92682477a9fb 100644 (file)
--- 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):