Clean confluence

A clean commit history for the confluence proof, along with the decision procedure for head normal form and some lemmas concerning the reflexive transitive closure.