Specify laws our primops obey

[kozross]

This is a good examples of what we need (towards the end of the section). Essentially, these are equational statements specifying what we can substitute. Some examples (not exhaustive):

• Idempotent abelian semigroup/monoid laws for AND, OR, XOR
• Self-inversion for complement
• Get-put, put-get and put-put laws for bit setting and reading
• De Morgan laws