Nested Implication

Hi Ben,

For the below property to be non vacuous what will be it changed too?
start |-> ##2 send |-> ##3 ack );