Notions of sameness need to be handled with care here in general. There are lots: literally identical code is the most obvious one, then provably identical behavior in PA (against some class of reasonable agents), then provably identical behavior in PA+1 (against some class of reasonable agents)… it’s sometimes necessary to use the first notion of sameness because opponents may not behave fairly, e.g. they may punish exactly one program, so in general the set of opponents you want to prove sameness with respect to also matters.
Notions of sameness need to be handled with care here in general. There are lots: literally identical code is the most obvious one, then provably identical behavior in PA (against some class of reasonable agents), then provably identical behavior in PA+1 (against some class of reasonable agents)… it’s sometimes necessary to use the first notion of sameness because opponents may not behave fairly, e.g. they may punish exactly one program, so in general the set of opponents you want to prove sameness with respect to also matters.
I believe this argument proves identical behavior against all modal agents, and identical behavior of modal agents against.