```
(def-theorem contains-an-element-implies-non-empty
"forall(x:uu, s:sets[uu], x in s implies nonempty_indic_q{s})"
(theory indicators)
(usages transportable-macete)
(proof
(

simplify
)))
```

```
(def-theorem is-singleton-implies-non-empty
"forall(a:uu, s:sets[uu],
nonempty_indic_q{indic{x:uu, x=a}})"
(theory indicators)
(usages transportable-macete)
(proof
(

direct-and-antecedent-inference-strategy
(instantiate-existential ("a"))
(apply-macete-with-minor-premises meaning-of-indic-from-pred-element)
simplify
)))
```

```
(def-theorem is-pair-implies-non-empty
"forall(a,b:uu, s:sets[uu],
nonempty_indic_q{indic{x:uu, x=a or x=b}})"
(theory indicators)
(usages transportable-macete)
(proof
(

direct-and-antecedent-inference-strategy
(instantiate-existential ("a"))
(apply-macete-with-minor-premises meaning-of-indic-from-pred-element)
simplify
)))
```

```
(def-theorem is-triple-implies-non-empty
"forall(a,b,c:uu, s:sets[uu],
nonempty_indic_q{indic{x:uu, x=a or x=b or x=c}})"
(theory indicators)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-existential ("a"))
(apply-macete-with-minor-premises meaning-of-indic-from-pred-element)
simplify
)))
```

```(def-script empty-set-handler 0
(
(let-macete non-empty-composite-macete
(series
tr%is-singleton-implies-non-empty
tr%is-pair-implies-non-empty
tr%is-triple-implies-non-empty))
(if (matches? "with(p:prop, p)"
"with(x:points, l:sets[points], x in l)")
(auto-instantiate-universal-antecedent
"with(l:sets[points],empty_indic_q{l})")
(block
(contrapose "with(l:sets[points],empty_indic_q{l});")
(backchain "with(s:sets[points],p:prop, s=indic{x:points, p})")
(apply-macete \$non-empty-composite-macete)))
))
```

```(def-script pick-an-element 0
(
(if (matches? "with(p:prop, p)"
"with(p:prop, not(forall(x:points, p)))")
(block
(contrapose "with(p:prop, not(forall(x:points, p)))")
insistent-direct-inference
(contrapose 0))
(skip))
))
```

```(def-script indic-handler 0
(
(if (matches? "with(l:sets[points],x:points,x in l)"
"with(p:prop, l:sets[points],l=indic{x:points,p})")
(block
(backchain "with(p:prop, l:sets[points],l=indic{x:points,p})")
(apply-macete-with-minor-premises indicator-facts-macete)
simplify)
(skip))))
```

```(def-script indic-removal 0
(
(if (matches? "with(p:prop,p)"
("with( x:points,p:prop,x in indic{y:points,p})"))
(block
(contrapose  ("with( x:points,p:prop,x in indic{y:points,p})"))
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce
(contrapose 0))
(skip))))
```

```(def-script indic-equality 0
(
(if (matches? "with(p:prop,indic{x:points,p}=indic{x:points,p})")

(block
extensionality
simplify
direct-and-antecedent-inference-strategy))))

```

```(def-script big-d-with-simplification 0
(
(label-node here)
direct-and-antecedent-inference-strategy
(label-node there)
(jump-to-node here)
(for-nodes
(unsupported-descendents)
simplify)
(jump-to-node there)))

```