Fixed two test cases by changing the Z3 prover. It now tries to rewrite goals of the shape: (∀x :: P) = (∀x :: Q) to (∀ x :: P = Q) when a first attempt has failed.