Parsing of quantifier on the right of binary connective should not need parentheses

The following proof leads to a parsing error

p v Ex5. x5 = x5 : sorry

while

p v (Ex5. x5 = x5) : sorry

is correctly parsed. The first snippet should also be accepted.