Bug with type polymorphism

[bmsherman]

This normal form is worrisome, with the F type variable left there. Even if perhaps that type variable doesn't matter, it's visually wrong.
The code comes from this definition:
https://github.com/psg-mit/marshall/blob/master/examples/cad.asd#L125-L128

# unit_cone;;
- : (real*real*real -> bool) -> bool = fun P : F -> bool => mkbool (forall x : [0.0, 1.] , forall x40 : [-1., 1.] , forall x24 : [-1., 1.] , 1. < x40 ^ 2 + x24 ^ 2 \/ is_true (P (x, x * x40, x * x24))) (exists x : [0.0, 1.] , exists x39 : [-1., 1.] , exists x23 : [-1., 1.] , x39 ^ 2 + x23 ^ 2 < 1. /\ is_false (P (x, x * x39, x * x23)))