Enable refinement by infix operators in prover

Fixes #873.