the Goal `∃ b, x ^ 2 + 2 * x = b` is solvable by `use x^2+2x`... Same with Pset 1 Level 1: `∃ a, f 3 = a`. (Thanks to [Piotr Skalski](https://x.com/PStilance))