Hi, > But I am still confused of the definition of `pre-wp`.. In the 2nd > line, `s` should have the type ∆(Val), mandated by `ϕ(s)`; and yet at > the same time `s` should have the type Res, from `s · rf`. May I ask if > what am I missing here? Right, that should have been ϕ(v)(s). Then things hopefully make sense... Kind regards, Ralf