Implement Part 2 in Ltac, to the degree this is possible.
Implement Part 2 in Ltac, to the degree this is possible.