Generated statements were actually ill-formed, since Coq 8.4 sometimes
interprets "A -> B <-> C" as "(A -> B) <-> C". (This bug was fixed in 8.5.)
We could print additional parentheses to work around the issue, but it is
about time we drop support for Coq 8.4 anyway.