`connective_dev` support ∃x. P(x) = ¬∀x . ¬P(x)
This pull request adds this case to Alethe: !24 (merged)
It seems it comes from veriT. This issue track whether it's supported in Carcara and Isabelle.
This pull request adds this case to Alethe: !24 (merged)
It seems it comes from veriT. This issue track whether it's supported in Carcara and Isabelle.