[kprovex] should warn/err when spec module doesn't include main-def-module

[radumereuta]

@emarzion ran into an interesting issue when trying to convert from kprove to kprovex:
https://github.com/kframework/kore/blob/master/test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k

$ cat path.k
module PATH
  import BOOL
  import INT
  syntax S ::= "a" | "b" | "c"
  rule a => b
endmodule

$ cat all-path-b-or-c-spec.k
module VERIFICATION
  imports PATH
endmodule

module ALL-PATH-B-OR-C-SPEC
  import PATH
  // This should be provable as transiting to b suffices
  claim <k> a => b #Or c </k> [all-path]
endmodule
$ kompile all-path-b-or-c-spec.k -m VERIFICATION --backend haskell
$ kprove all-path-b-or-c-spec.k // works fine
$ kprovex all-path-b-or-c-spec.k // error
syntax error, unexpected character `<`

The problem is the proof module doesn't include the main definition module where the configuration was built.
Does it make sense to warn/err when the main def module is not included in the spec modules?

[radumereuta]

Most likely a won't fix.
The syntax error was because the configuration syntax was not being imported.
Giving a more intuitive error message would require a bit too much work, and we get a decent error message now.