Definition of weak-head-reduction and proof of unicity of derivations

[mattam82]

Weak-head reduction is defined just like red1 without the congruence rules. To show a standardization theorem on it we'll need to show that it commutes with "internal" reduction that just does the missing congruences.