((([a]p0) \/ ([b]p1)) -> (<b>p0) \/ (<a>p1)) -> ([d]((p0 /\ (p0 -> ([a]p0)))-> ([a]p0)))