metis encoder can't deal with bare applications to quantifier.

[ordinarymath]

Metis can't prove this 2 theorems

METIS_PROVE[]``$? $¬`` (*Fails*)
METIS_PROVE []``¬$! $¬``  (*Fails*)

This is not an issue with metis but with the encoder. metis can prove the abstracted version.

METIS_PROVE[]``?x. ¬ x`` (*Succeeds*)

[mn200]

I view this as a feature request to improve/adjust the metis-encoder.