Explicit forall in lemmas

Currently, Prosa adheres to the following style

Lemma my_lemma : forall foo (bar : foo) x y z, property bar x y z.
Proof.
move=> foo bar x y z.

which is strictly equivalent to the (more concise but less explicit)

Lemma my_lemma foo (bar : foo) x y z : property bar x y z.
Proof.

Should we keep enforcing the explicit forall style? We could either:

• keep enforcing the explicit forall style
• keep enforcing it only for basic definitions (behavior for instance)
• no longer enforce it