title: Symbolic theory proving using SBV and Haskell
body: <p>I'm using <a href="http://leventerkok.github.io/sbv/">SBV</a> (with Z3 backend) in Haskell to create some theory provers. I want to check if forall <code>x</code> and <code>y</code> with given constrains (like <code>x + y = y + x</code>, where <code>+</code> is a "plus operator", not addition) some other terms are valid. I want to define axioms about the <code>+</code> expression (like associativity, identity etc.) and then check for further equalities, like check if <code>a + (b + c) == (a + c) + b</code> is valid formal <code>a</code>, <code>b</code> and <code>c</code>.</p>
  
  <p>I was trying to accomplish it using something like:</p>
  
  <pre><code>main = do
      let x = forall "x"
      let y = forall "y"
      out &lt;- prove $ (x .== x)
      print "end"
  </code></pre>
  
  <p>But it seems we cannot use the <code>.==</code> operator on symbolic values. Is this a missing feature or wrong usage? Are we able to do it somehow using SBV?</p>