start on proof of normalize. i think my definition is too complicated to prove things about; not sure what to do next. start on last 2 exercises (informal proofs)