Fix the bug in the equality substitution by making sure that the rewrite of equalities works.
Add the parametric kinds to the Boolean term converter to avoid taking the type of parametric operators.