Don't include constraints for variables just mentioned in the proof, not the hypotheses or conclusion.
This is a jhilbert/ghilbert difference.
Don't try (poorly) to handle constraints with more than two variables.