The translator accepts constants with preconditions

The translator accepts constants with preconditions, and duplicates preconditions:

```sml
> val foo_def = Define` foo = 5 DIV 0`;

Definition has been stored under "foo_def"
val foo_def = [] ⊢ foo = 5 DIV 0: thm
```

```sml
> val th = translate foo_def;

Translating foo

WARNING: foo has a precondition.

val th = [foo_side, PRECONDITION foo_side] ⊢ NUM foo foo_v: thm
```

What's worse, the precondition also leaks into the theorem produced by `ml_progLib`:
```sml
> get_ml_prog_state() |> ml_progLib.get_thm;
val it = [foo_side] ⊢ ... ... [... ] (scratch_st ffi): thm
```