The idea is to just drop y, since it is implicit in Hy.
Note that in theory we could also drop P and W since they also appear in Hy, but this might be confusing.
Reserved Notation "P '`^^' W '(' x '|' Hy ')'".
Reserved Notation "P ''_' n0 '`^^' W '(' a '|' Hy ')'".
Lemma ppE (x : 'rV[A]_n) (y : 'rV[B]_n) (Hy : receivable W P y) :
P `^^ W (x | Hy) = \Pr_(`J(P, W ``^ n))[[set x]|[set y]].
The idea is to just drop
y, since it is implicit inHy. Note that in theory we could also dropPandWsince they also appear inHy, but this might be confusing.