In Main: moved Bin to the left to preserve the solver in its simpset.
datatype
'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
| Sum ('a aexp) ('a aexp)
| Diff ('a aexp) ('a aexp)
| Var 'a
| Num nat
and 'a bexp = Less ('a aexp) ('a aexp)
| And ('a bexp) ('a bexp)
| Neg ('a bexp)