Fixed (?): Truth of (x. P(x)) v (Ex. ~P(x)).

The reason why this is provable is our different treatment of standard
names. The old one was wrong anyway, because fol_inconsistency_reverse
test came out false, i.e., (x. P(x)) v (y. ~P(y)) came out true.

Important open questions:
 * Is our substitution mechanism sound?
 * Is it necessary and/or sufficient to re-use placeholder standard
   names from the setup for the query?