update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index aabb5adae086e3bf10d98b1fe4f87783c8c3bda1..4ce09045380a7366bf8aefe467ade8f7baa14e60 100644 (file)
--- 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)"