I am trying to prove a lemma by "coinduct".
I get the following error, at the point when I call "proof coinduct"
*** exception TERM raised: Expected 3 binop arguments
*** At command "proof".
What kind of error is that? any clue?
Thanks in advance for any advice.