How to formalize this def.
Given a tree, I want to define something in function of node A and node B such that: A->B path exists and it is of length = 1 (either B is parent of A or one of its children). I came up with something raw: ∃ A->B AND (A->B).length = 1, but I don't think that's the proper way.