The conv tactic provides a conv within a conv. It allows the user to return to a
previous state of the outer conv block to continue editing an expression without having to
start a new conv block.
guard_target t fails if the target of the conv goal is not t.
We use this tactic for writing tests.