fix show-refinement when dual chc is used

[KenSakayori]

The show-refinement option did not show the correct type when the solver used the dual formula to solve the original problem. The issue was that the "refinement formulas" were not negated when it was printed. This PR fixes this issue.

For example, if

Sentry =v
     ∀ i . ∀ n . i >= n \/ (
         ∀ u1 . ∀ u2 . 5 > u1 \/ 5 > u2 \/ 2*i - u1 > -5 \/ 2*i + u1 < 5 \/ 2*n - u1 > -5 \/ 2*n + u1 < 5 \/ 2*i - u2 > -5 \/ 2*i + u2 < 5 \/ 2*n - u2 > -5 \/ 2*n + u2 < 5 \/ P u1 u2 i 0 n
    ) .
 P u1 u2 i j n =v
     u1 > 0 /\ u2 > 0 /\ (
         i >= j \/ i - n >= -1 \/ P ( u1 - 1 ) u2 0 n ( 1 + i ) \/ (
             ∀ f . 5 > f \/ 2*i - f > -7 \/ 2*i + f < 3 \/ 2*n - f > -5 \/ 2*n + f < 5 \/ P f ( u2 - 1 ) ( 1 + i ) 0 n
        )
    ) /\ (
         i - j <= -1 \/ P ( u1 - 1 ) u2 ( 1 + j ) n i \/ (
             ∀ f . 5 > f \/ 2*i - f > -5 \/ 2*i + f < 5 \/ 2*n - f > -5 \/ 2*n + f < 5 \/ 2*j - f > -7 \/ 2*j + f < 3 \/ P f ( u2 - 1 ) i ( 1 + j ) n
        )
    ) .

was given as an input and show-refinement was used, the refinement type for Sentry was printed as *[ff], but now *[tt] is printed. (BTW please use --solver=eld for this problem.)

This is a commit based on https://github.com/hopv/rethfl/commit/ac75736aca9c1b4b592615efb08da7baea5019a6. It is simpler than the original commit, however. The original commit also deals with type annotations, but the codes for type annotations have been removed simply because we do not support it yet. I'm aware that cherry-picking commits in a nonchronological order causes a mess, but I wanted to have this bug fixed.