Syntax of Solvent properties

[bitbart]

Simplify the syntax of Solvent properties as follows:

1. Always omit the st. prefix
2. Replace app_tx_st with <tx>
3. Replace the logical operator not with ! (see related issue on Solidity syntax)
4. Allow omitting Forall xa when xa does not occur in the formula

For example, consider the following property in the current Solvent syntax:

Forall xa [
not target_reached && st.block.number > st.end_donate
-> Exists tx [1, st.owner]
[ app_tx_st . balance [st.ower] >= st.balance [st.owner] + st.donors[st.owner] ] ]

After applying the 4 simplifications above, this is rewritten as follows:

!target_reached && block.number > end_donate
-> Exists tx [1, owner]
<tx> balance[ower] >= balance[owner] + donors[owner]