title: apply associativity in CafeOBJ
body: <p>I need (as a part of larger proof) to proove that a * (b * c) equals (a * b) * c which is true because * is declared associative.
  I can <em>match</em> one term with another but it is not what I need because I need to write a proof score in form</p>
  
  <pre><code>start
  ...
  close 
  </code></pre>
  
  <p>so I need to use <em>apply</em> or something like.</p>
  
  <p>What I've tried is to mark associativity as an axiom:</p>
  
  <pre><code>eq [assoc] : x:Elt * (y:Elt * z:Elt) = (x * y) * z .
  </code></pre>
  
  <p>but I cannot <em>apply</em> it then either because I cannot substitue multiple arguments </p>
  
  <pre><code>%MONOID&gt; show term
  
  (c * (a * b)):Elt
  
  %MONOID&gt; apply -.assoc with x = a y = b z = c at term .
  
  [Error] no successful parse
  [Error]:
  </code></pre>
  
  <p>or maybe because this rule is marked as invalid (what is reported while applying other rules ):</p>
  
  <pre><code>** id-completion for rule: eq [assoc]: (x:Elt * (y:Elt * z:Elt)) = ((x * y) * z)
  
    -- Generated rules:
    none
    -- Generated, but invalid rules:
    eq [assoc]: (x:Elt * (y:Elt * z:Elt)) = ((x * y) * z)
  </code></pre>
  
  <p>how to apply associativity and how to apply equation with multiple arguments (cant find this in docs <a href="http://cafeobj.org/files/reference-manual.html#apply" rel="nofollow">http://cafeobj.org/files/reference-manual.html#apply</a> <a href="http://cafeobj.org/files/manual.pdf" rel="nofollow">http://cafeobj.org/files/manual.pdf</a> ) ?</p>