Fix some mistakes in the Shelley formal spec

[javierdiaz72]

The following mistakes in the Shelley formal specification shall be fixed:

1. Figure 69: Instead of $ℙ\;PrtclEnv$, it should say $PrtclEnv$.
2. Section 12.13: Instead of "It calls BHEAD, PRTCL, and BBODY as sub-rules." it should say "It calls TICK, TICKN, PRTCL, and BBODY as sub-rules."; and similarly in the introduction paragraph of Section 12.
3. Figure 75: It should say $(e_2, \_, b_{cur}, es, \_, pd)$ instead of $(e_2, \_, b_{cur}, es, \_, \_, pd)$, and $\mathsf{bhash}\;bhb$ instead of $\mathsf{bhash}\;bh$.
4. Figure 5: The function $\mathsf{vrf}_\mathsf{T}$ returns a value of type $\mathsf{T} \times \mathsf{Proof}$ but the function $\mathsf{verifyVrf}_\mathsf{T}$ expects a value of type $\mathsf{Proof} \times \mathsf{T}$, therefore the expression $\mathsf{verifyVrf}_\mathsf{T}\;vk\;seed\;(\mathsf{vrf}_\mathsf{T}\;sk\;seed)$ is ill-typed. When fixing this, we shall take into account the uses of $\mathsf{verifyVrf}_\mathsf{T}$ in Section 12.9.