finished the proof search for foralls, exists might be broken