Universally (existentially) quantify leftover variables in proof (sat-check). Also, add some nasty test cases where this is needed.