Figured out one of Imp problems, will attempt similar approach for second problem.
Worked through more of the Hoare.v exercises.