Introduces a guiding witness, indicating what the original solution was.
This original solution is then either

1) tried as potential solution (verification)
2) used as decomposition, for instance on If expressions.