Fixed typos; improved whnf term equivalence rules
Added most of term equivalence, except for J