Put `Φ` of `frame_fractional` first to make it easy to specify it if Coq fails to infer it.
This is a follow up of !928 (merged). While porting reverse dependencies we noticed that Coq is not always able to infer the Φ, see simuliris@c0dff161 for an example.
This MR makes it easier to specify the Φ, you can write apply: (frame_fractional (λ q, ...)) instead of apply: (frame_fractional _ _ _ (λ q, ...)).
Edited by Robbert Krebbers