Check game-theoretic safety properties

[fare]

The main advantage of our approach over that of other people who use formal methods to verify smart contracts is that we have this explicit notion of multiple participants, out of which we can extract game-theoretic safety properties for each participant, that are not expressible in participant-agnostic formalisms. Let's make sure we prove at least some such properties for RPS and have a way to express them explicitly if we cannot derive them fully implicitly.

[fare]

The possible? and eventual? predicates in an @A block, or a variant thereof, should be adversarial: it should take into account the fact that B will actively try to make it not happen.

[fare]

Do something with the correct quantifiers for now. See #166 for the next level.

[fare]

Also, Jay's fair_game predicates are extremely round about. Hopefully, it should be possible to say at a point before A choses his hand something like possible? (outcome == A_WINS), which either assumes the content inside possible? is all-seeing of the bindings at the end of the interaction, or we have an explicit label feature and COMEFROM feature such that we can express possible? END(outcome == A_WINS) at the point where we assert it's a possible future.

Then there's the matter of the quantifiers: existence with or without a winning strategy, against or not against the other participant's winning strategies.