Some notation changes (incl. A_x for ancestors(π,x))
Merged
More notation tweaks (replacing \(...\) with \HOLtm mostly)