[dabrahams]

…and all the consequences of those corrections. Also delete needless caveats
about composability, since that has been demonstrated.

f upholds P means given any finite trace b s.t. b |= P, f(b) |= P
where f(b) is the behavior prefix that starts with the behavior prefix b and continues with the states produced by
applying f in b's final state.

Given the above, if f upholds P and g upholds P, for any finite behavior prefix b s.t. b |= P:
f(b) = b' |= P
b' |= P => g(b') |= b
thus g(f(b)) |= P.

Thus anything that does not compose is not a Lamport property.

Fixes #52

[dabrahams]

@sean-parent gentle bump