Ref Man for my contribution

I'll be happy if this could be proofread before I merge ...
I think you should put in `by \texttt{simpl} nor \textt{cbn}`; they will still be unfolded by `lazy`.