Existential Quantification

[CodaFi]

Using the equivalence

∃ {x} . P x ≡ ¬ ∀ {x} . ¬ P x

Define the inverse of a property. From there, negate on the inside and outside and define existential quantification.

[CodaFi]

From there use

∃! {x} . P x ≡ (P x /\ ¬ ∃ {y} . (P y /\ y ≠ x))

For uniqueness.

[CodaFi]

So this says... We expectFailure on the property then expectFailure on each test case. Seems awfully wasteful. Must disable shrinking too while we're at it ('cause it doesn't make sense). Will have to bring back once.

[CodaFi]

What if...

Isn't this just (extensionally) the same as expectFailure on the outside. Then we let the shrinker loop search for a minimum passing value and map it back to success.