recursive calls when removing unknowns us missing

now we have proof that those remove unknowns really remove all unknowns

TODO: rerun test, check if everything proofchecks again