Proof obligations for the second method.