Remove UnificationError

[ttuegel]

The possibility of having a UnificationError exists for instantiating rewrite rules and signals that the backend did not completely solve a unification problem. However, this condition is already detected by the substitution coverage check! We do not need to do any error handling in the unification code itself, rather we only need to check this post-condition: that unification produced a substitution for every variable.