Let x be given.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
rewrite the current goal using Hxkm (from left to right).
∎