`progress ... with` require a context hypothesis to proceed in some cases

[RaitoBezarius]

trafficstars

In https://github.com/RaitoBezarius/avl-verification/blob/avl/Verification/Rotate.lean#L43-L44, we can see this proof code:

have := AVLNode.update_height_spec a h left_right right
progress keep Hupdate₁ with AVLNode.update_height_spec as ⟨ t_new₁, H₁ ⟩

This is a weird situation because the this hypothesis is necessary (if you remove it, the proof code breaks) even though there's an explicit use of with which should give the specification to use.