Rework the formula predicates:

       - adds testing for first child, next sibling etc and their converse
       - make the predicate complete w.r.t negation
       - move the evaluation of formula to the Eval module (where the type of
       context is known)