Menu
▾
▴
#364 Infer existential from set cardinal
Julien Cervelle and Frédéric Gervais report that, given a set E such that card(E)≥2, Rodin is not able to infer that ∃x,y·x∈E∧y∈E∧x≠y.
However, a similar goal works well for sets with at least one element: Rodin can deduce that ∃x·x∈E from card(E)≥1. It would be useful to generalize it for sets with more than one element.
This would be a new reasoner / tactic.