Skip to content

`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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information