Change the concrete syntax for implication to ==> instead of => that we use now. This has better readability and less ambiguity.

Change the symbol for storage update to := instead of => that we use now. This make the syntax consistent with the ones for constructors. I also find this more intuitive.