X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpreterm.ma;h=4ce09045380a7366bf8aefe467ade8f7baa14e60;hb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;hp=aabb5adae086e3bf10d98b1fe4f87783c8c3bda1;hpb=291fe1d3b56faf91d07099f43f3ebde2988649e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index aabb5adae..4ce090453 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -23,14 +23,14 @@ include "delayed_updating/notation/functions/uptriangle_1.ma".
 definition preterm: Type[0] ≝ 𝒫❨path❩.
 
 definition preterm_grafted: path → preterm → preterm ≝
-           λp,t,q. p;;q ϵ t.
+           λp,t,q. p●q ϵ t.
 
 interpretation
   "grafted (preterm)"
   'Pitchfork t p = (preterm_grafted p t).
 
 definition preterm_root: preterm → preterm ≝
-           λt,q. ∃r. q;;r ϵ t.
+           λt,q. ∃r. q●r ϵ t.
 
 interpretation
   "root (preterm)"