module M {
    spec module {
        invariant forall x: num y: num : x == y;
    }
}