This is known to be an issue with the json output, but perhaps it applies more widely.
Currently proofs only include a line number, which is not enough to disambiguate and pinpoint when multiple proofs are present in a single source line.
It is not clear to me if we need to do something special in the presence of macros?