>If the proof covers all of that then it's not strictly needed, but it's cheap paranoia.
Do you mean id/actor/to of a plaintext activity, or of an envelope (EncryptedActivity)?
My understanding is that the properties of an envelope have no effect on security. It can even have a different actor.
I added an example of a plaintext activity: https://codeberg.org/silverpill/feps/src/branch/main/0806/fep-0806.md#plaintext-activity
Also added HPKE mode to the parameter list - mode_base.

