*: use ? for variables introduced in RHS

[asymmetric]

Should fix some of the warnings at the bottom.

There are more cases that I found less straightforward, like when it complains about _ => _ - I haven't fixed those.

Here is the documentation of the new syntax.

[asymmetric]

These rules also seem problematic, given that D is not defined:

rule  A -Int ( (B /Int 64)  +Int C) => (0 -Int ( (B /Int 64) -Int (A -Int C)))
    requires (notBool #isVariable(A))
    andBool (notBool #isConcrete(A))
    andBool (A =/=K (D /Int 64))
rule  A -Int ( (B /Int 64)  -Int C) => (0 -Int ( (B /Int 64) -Int (A +Int C)))
    requires (notBool #isVariable(A))
    andBool (notBool #isConcrete(A))
    andBool (A =/=K (D /Int 64))
rule  A +Int ( (B /Int 64) +Int  C) => (B /Int 64) +Int (A +Int  C)
    requires (notBool #isVariable(A))
    andBool (notBool #isConcrete(A))
    andBool (A =/=K (D /Int 64))
rule  A +Int ( (B /Int 64) -Int  C) => (B /Int 64) +Int (A -Int  C)
    requires (notBool #isVariable(A))
    andBool (notBool #isConcrete(A))
    andBool (A =/=K (D /Int 64))

Haven't looked at them deeply enough to be able to tell what they should look like. Are they OC?

[kmbarry1]

So, I didn't notice this existed until I was nearly done with #414, but I went ahead and opened that since there's a lot more to fix than what's in this PR so far...if this is still being worked on, happy to close #414 and let this play out.