Expose memory binding(s) in program logic statements

[oskgo]

This is a follow up PR to #789 that now allows the user to decide the name of the memory bound by a program logic statement or probability expression. This makes nested program logic statements clearer.

The syntax is {&my_memory} after the procedures (and arguments for a Pr) (for the relevant side if two-sided).
Examples:

• hoare[P.p {&m}: true ==> true]
• Pr[P.p(a) {&end_mem} @ &start_mem: true] = 0%r
• equiv[P.p {&left} ~ P.p {&right}: true ==> true]

The change is backwards compatible since it is optional to provide the memory. If not provided a default name will be used instead (&hr for one-sided cases and &1/&2 for left/right in two-sided cases). The pretty printer omits the memory binding if the default names are used.

Some tactics (conseq?) will probably also want an optional memory parameter, but I'd rather deal with that as needed.