add example showing why we cannot simply extract the witness from TerminatesWith...
[coinductive-monad.git] / Computation / Tactics.v
2007-10-02 adamrename Recursion