#380 Contradiction with set membership

[Guillaume Verdier]

If a proof has two hypotheses like x = a and x ≠ a, the prover automatically finds the contradiction and proves the goal. It would be useful to extend this to set membership, such that hypotheses like x ∈ {a, b} and x ∉ {a, b, c} could be automatically detected as a contradiction.
This was first requested by Jean-Paul Bodeveix and Mamoun Filali.