Is the signature of Later_From in def 4.5 correct?

[yudetamago]

Hi, now I try to do cbc casper formal verification by using Isabelle (see: https://github.com/LayerXcom/cbc-casper-proof). I noticed that the signature of Later_From in definition 4.5 seems wrong.

Later and From_Sender are defined as follows.

Later: M * P(M) -> P(M)
From_Sender: V * P(M) -> P(M)

So I think Later_From should be defined as:

Later_From: M * V * P(M) -> P(M)

How do you think?