Gave a proof for the very first case: => with P_True.
Most of this can probably be generalized for many of the other cases.