gh_ex only accepts a single argument
clayrat opened this issue · 1 comments
clayrat commented
This forces us to bundle logical variables into one, so that they can be passed to gh_ex in a proof. model.gE from FCSL can accept multiple arguments by packaging them in a nested existential.
aleksnanevski commented
It isn't just gh_ex, also the syntax for STsep types.