make <==> chain like ==. or making chaining <==> an error

[kjx]

I remembered <==> has a lower binding strength than ==, but not that <==> didn't chain.
Debugging something like this took me an hour or so.

an obvious solution is to either make <==> chain like == or making chaining <==> an error

lemma chain(a : bool, b : bool, c : bool)
  requires a <==> b 
  requires b <==> c
  ensures  a  ==  b  ==  c
  ensures  a <==> b <==> c
  {}

I honestly can't understand why one would write a <==> b <==> c meaning a <==> (b <==> c) ---especially when both brackets and a <==> b == c is available for the other sense.