Improved the prover. When discharging a proof obligation of the form x R y, with R ∈ { =, ⇒ }, if x and y share some structure, z3 will be given a list of goals with a choice of which one to prove.