diff --git a/Language/Memo/Ztrategic.hs b/Language/Memo/Ztrategic.hs
--- a/Language/Memo/Ztrategic.hs
+++ b/Language/Memo/Ztrategic.hs
@@ -239,3 +239,23 @@
 --Apply a function with access to the zipper, fail the composition if it fails
 monoTUZ :: (MonadPlus m, Typeable a, Typeable d, Typeable mm) => (a -> Zipper (d mm) -> (m r, Zipper (d mm))) -> TU m r
 monoTUZ = adhocTUZ failTU
+
+
+{-
+New! Useful to express properties.
+-}
+
+forallNodes :: (Typeable a, Data (d mm), Memoizable d mm, StrategicData (d mm)) => (a -> Zipper (d mm) -> ([Property], Zipper (d mm))) -> d mm -> Property
+forallNodes p ast = let 
+     astZipper = toZipper ast
+     step = failTU `adhocTUZ` p
+     (props, _) = applyTU (full_tdTU step) astZipper
+    in conjoin props
+
+
+existsNode :: (Typeable a, Data (d mm), Memoizable d mm, StrategicData (d mm)) => (a -> Zipper (d mm) -> ([Property], Zipper (d mm))) -> d mm -> Property
+existsNode p ast = let 
+     astZipper = toZipper ast
+     step = failTU `adhocTUZ` p
+     (props, _) = applyTU (full_tdTU step) astZipper
+    in disjoin props
diff --git a/Language/Ztrategic.hs b/Language/Ztrategic.hs
--- a/Language/Ztrategic.hs
+++ b/Language/Ztrategic.hs
@@ -335,6 +335,28 @@
 allTUright :: Monoid (m d) => TU m d -> TU m d
 allTUright f = MkTU $ \z -> moveQ right mempty (applyTU f) z
 
+breadthFirst_tdTU :: (Monoid (m d)) => TU m d -> TU m d
+breadthFirst_tdTU f = MkTU $ \z -> bf' f z [(id, id)]
+ where bf' f z [] = mempty
+       bf' f z ((trav, untrav):travs) =
+           do
+             -- for this node (as in, the node this function is working on)
+             let thisNode = trav z
+             -- compute its value
+                 thisNodeValue = applyTU f thisNode
+             -- prepare navigation functions to traverse immediate children
+             let newTravs = gatherChildren (trav, untrav) thisNode
+             -- back to the initial node (exactly the same as z in a TU traversal...)
+             -- here we could just use z instead of baseTransformed
+             -- but i keep it similar to the TP strategy for consistency
+                 baseTransformed = untrav thisNode
+             -- recursive calls, first into the remaining traversals `travs`
+             -- and only after into the children `newTravs` we computed above 
+                 recurse = bf' f baseTransformed (travs ++ newTravs)
+             -- finally, join all results with `mappend` (generic monadplus ++ operation)
+             thisNodeValue `mappend` recurse
+
+
 adhocTU :: (Monad m, Typeable a) => TU m d -> (a -> m d) -> TU m d
 adhocTU f g = MkTU $ \z -> fromMaybe (applyTU f z) (getHole z >>= return . g)
 
@@ -363,3 +385,23 @@
 
 monoTUZ :: (MonadPlus m, Typeable a, Typeable e) => (a -> Zipper e -> m d) -> TU m d
 monoTUZ = adhocTUZ failTU
+
+
+{-
+New! Useful to express properties.
+-}
+
+forallNodes :: (Typeable a, Data b, StrategicData b) => (a -> Zipper b -> [Property]) -> b -> Property
+forallNodes p ast = let 
+     astZipper = toZipper ast
+     step = failTU `adhocTUZ` p
+     props = applyTU (full_tdTU step) astZipper
+    in conjoin props
+
+
+existsNode :: (Typeable a, Data b, StrategicData b) => (a -> Zipper b -> [Property]) -> b -> Property
+existsNode p ast = let 
+     astZipper = toZipper ast
+     step = failTU `adhocTUZ` p
+     props = applyTU (full_tdTU step) astZipper
+    in disjoin props
diff --git a/Ztrategic.cabal b/Ztrategic.cabal
--- a/Ztrategic.cabal
+++ b/Ztrategic.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.37.0.
+-- This file has been generated from package.yaml by hpack version 0.38.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:           Ztrategic
-version:        0.2.0
+version:        0.3.0
 synopsis:       Zipper-based library for strategic programming and attribute grammars.
 description:    Strategic programming and attribute grammar library built on top of the Zipper data structure. Can be used as a strategic programming library exclusively, with the option of integrating attribute grammars during strategic term traversal. Supports non-memoized and memoized attribute grammars. 
 category:       Generics