Added naïve (non-compiling) definitions / fixpoints.
And updated the problem section of the README accordingly.
Problem is that step can't be defined as a fixpoint decreasing on some argument.