Properly implement equality meta-variables, or at least hack them correctly

[andrejbauer]

In nucleus/meta.ml, when we form_meta, it seems strange that the equalities formed by meta-variables have empty assumption sets (should it not be the singleton mv?) Or maybe the correct thing to do is to have constructors for equality meta-variables in eq_term and eq_type?

[andrejbauer]

Here's a worrisome example:

# rule A type
Rule A is postulated.
# rule B type
Rule B is postulated.
# let r = ref ML.None
val r :> ref (ML.option _α) = ref<0>
# derive (A == B as xi) -> (r := ML.Some xi; xi)
- : derivation = derive (A ≡ B as xi) → A ≡ B
# !r
- : ML.option judgement = ML.Some (⊢ A ≡ B)

The point is that we have now derived ⊢ A ≡ B without any assumptions.

[andrejbauer]

Fixed by f44f4fc