Pure構文、ほんとに意味不明

一番上はOK、NGとコメントしてあるのは構文エラー

definition "right_unit_law == (!!n.(n + 0 == n))"

definition "right_unit_law1 == !!n.(n + 0 == n)" (* NG *)
definition "right_unit_law2 == (!!n. n + 0 == n )"
definition "(right_unit_law3) == (!!n.(n + 0 == n))"
definition "(op ==) right_unit_law4 (!!n.(n + 0 == n))" (* NG *)

definitionで使う == は、オペレータではなくて、区切り記号なのだろう。よって、最後がNGは分かる。二番目のNGは分からない。!!n.(n + 0 == n) は式として正しい。だが、定義の右辺になれない。括弧付ける必要がある、って何故？

[追記]==が左結合的だからだろう。だが、最初に出現する == は区切り記号で、オペレータの意味がないのなら、結合性をどうこう言ってもしょうがない、と思う。パーザーの実装上の都合か。

定義の際に、オペレータである==の記号を区切り記号に流用したことが、そもそも変だと思う。[/追記]