Prove nf_recursion, stronger nog_ns, some new alist lemmata.