Incorrect output of obligation that includes `\lnot` on an unbound variable

[ahelwer]

Reproduced with 202210041448 release. Running tlapm on:

---- MODULE NegLeq ----
EXTENDS Naturals
VARIABLES i, f
THEOREM ~(i <= f) <=> i > f
  PROOF OBVIOUS
====

will output:

tlapm NegLeq.tla
(* loading fingerprints in ".tlacache/NegLeq.tlaps/fingerprints" *)
(* created new ".tlacache/NegLeq.tlaps/NegLeq.thy" *)
(* fingerprints written in ".tlacache/NegLeq.tlaps/fingerprints" *)
File "./NegLeq.tla", line 5, characters 9-15:
[ERROR]: Could not prove or check:
           ASSUME NEW VARIABLE i,
                  NEW VARIABLE f
           PROVE  ~i =< f <=> i > f
File "./NegLeq.tla", line 1, character 1 to line 6, character 77:
[ERROR]: 1/1 obligation failed.
There were backend errors processing module `"NegLeq"`.
 tlapm ending abnormally with Failure("backend errors: there are unproved obligations")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm.process_module in file "tlapm.ml", line 408, characters 12-77
Called from Tlapm.main.f in file "tlapm.ml", line 503, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 506, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33

Of course the above proof only succeeds if <= and > are defined over a set that is totally ordered like Nat, but I thought the obligation output might be indicative of a bug lurking; see that the parentheses were ignored:

~(i <= f) <=> i > f

became

~i =< f <=> i > f

[ahelwer]

Actually nevermind, this is just because \lnot has precedence 4-4 and <= has precedence 5-5, so ~i =< f <=> i > f and ~(i <= f) <=> i > f are the same expression. Somewhat surprising but whatever.