Removed test code.
Added normalization, with beta and definition substitution. Does not work.