Simplified normalizer by giving up on termination

It's not the purpose of this construction to prove termination for a calculus
that obviously terminates. It's easier to use a PHOAS encoding for our purposes.