```
(def-theorem defined-iota-expression
"forall(p:[ind_1,prop],
#(iota(i:ind_1,p(i)))
implies
(p(iota(i:ind_1,p(i))) and
forall(j:ind_1, p(j) implies j=iota(i:ind_1,p(i)))))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-inference
direct-inference
(cut-with-single-formula
"#(iota(i:ind_1,p(i))) and forall(x:ind_1,x=x)")
(contrapose "with(i:ind_1,#(i));")
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,p or p);")
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(eliminate-iota 0)
(instantiate-existential ("y%iota")))
(block
(script-comment "`direct-inference' at (1)")
(instantiate-universal-antecedent-multiply
"with(y%iota:ind_1,p:[ind_1,prop],
forall(z%iota:ind_1,p(z%iota) implies z%iota=y%iota));"
(("j") ("iota(i:ind_1,p(i))")))
direct-inference
direct-inference)
)))
```

```
(def-theorem defined-iota-expression-satisfiability
"forall(p:[ind_1,prop],
#(iota(i:ind_1,p(i))) implies p(iota(i:ind_1,p(i))))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression ("p"))
)))
```

```
(def-theorem defined-iota-expression-existence
"forall(p:[ind_1,prop],
#(iota(i:ind_1,p(i))) implies nonvacuous_q{p})"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression ("p"))
auto-instantiate-existential
)))
```

```
(def-theorem defined-iota-expression-full-existence
"forall(%%p%%:[ind_1,prop],
not(#(iota(i:ind_1,%%p%%(i))))
or
forsome(j:ind_1,
j=iota(i:ind_1,%%p%%(i)) and %%p%%(j) and forall(j_1:ind_1, %%p%%(j_1)
implies
j=j_1)))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression ("%%p%%"))
auto-instantiate-existential
(instantiate-universal-antecedent
"with(%%p%%:prop, forall(j:ind_1,%%p%%))" ("j_\$0"))
)))
```

```
(def-theorem defined-iota-expression-uniqueness
"forall(p:[ind_1,prop],
#(iota(i:ind_1,p(i)))
implies
forall(j:ind_1, p(j) implies j=iota(i:ind_1,p(i))))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression ("p"))
(backchain "with(p,q:prop, forall(j:ind_1, p implies q))")
)))
```

```
(def-theorem defined-iota-expression-iota-free-uniqueness
"forall(p:[ind_1,prop],
#(iota(i:ind_1,p(i)))
implies
forall(i,j:ind_1, (p(i) and p(j)) implies i=j))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression ("p"))
(instantiate-universal-antecedent-multiply
"with(p:prop,forall(j:ind_1,p));"
(("i") ("j")))
)))
```

```
(def-theorem equal-iota-expressions-lemma
"forall(p,q:[ind_1,prop],
iota(i:ind_1,p(i)) = iota(i:ind_1,q(i))
implies
forall(k:ind_1, p(k) implies q(k)))"
lemma
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression-uniqueness ("p"))
(instantiate-universal-antecedent "with(p:prop, forall(j:ind_1,p))" ("k"))
(force-substitution "k" "iota(i:ind_1,q(i))" (0))
(apply-macete-with-minor-premises defined-iota-expression-satisfiability)
)))
```

```
(def-theorem equal-iota-expressions
"forall(p,q:[ind_1,prop],
iota(i:ind_1,p(i)) = iota(i:ind_1,q(i)) implies p=q)"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
direct-inference
simplify
(instantiate-theorem equal-iota-expressions-lemma ("p" "q"))
(instantiate-theorem equal-iota-expressions-lemma ("q" "p"))
(instantiate-universal-antecedent
"with(p,q:[ind_1,prop],forall(k:ind_1,q(k) implies p(k)));" ("x_0"))
(instantiate-universal-antecedent
"with(q,p:[ind_1,prop],forall(k:ind_1,p(k) implies q(k)));" ("x_0"))
simplify
simplify
)))
```

```
(def-theorem defined-iota-expression-elimination
"forall(p:[ind_1,prop],
#(iota(i:ind_1,p(i)))
iff
forsome(i:ind_1, p(i) and forall(j:ind_1, p(j) implies j=i)))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression-full-existence ("p"))
(instantiate-existential ("j"))
(instantiate-universal-antecedent
"with(p:prop, forall(j_1:ind_1,p))" ("j_\$0"))
(eliminate-iota 0)
auto-instantiate-existential
direct-and-antecedent-inference-strategy
(instantiate-theorem defined-iota-expression-full-existence ("p"))
(instantiate-existential ("j"))
(instantiate-universal-antecedent
"with(p:prop, forall(j_1:ind_1,p))" ("j_\$0"))
)))
```

```
(def-theorem negated-defined-iota-expression-elimination-1
"forall(p:[ind_1,prop],
forall(i:ind_1, not(p(i)))
implies
not(#(iota(i:ind_1,p(i)))))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
(contrapose "with(p:[ind_1,prop],forall(i:ind_1,not(p(i))));")
auto-instantiate-existential
)))
```

```
(def-theorem negated-defined-iota-expression-elimination-2
"forall(p:[ind_1,prop],
forsome(i,j:ind_1, p(i) and p(j) and not(i=j))
implies
not(#(iota(i:ind_1,p(i)))))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(instantiate-universal-antecedent-multiply
"with(y%iota:ind_1,p:[ind_1,prop],
forall(z%iota:ind_1,p(z%iota) implies z%iota=y%iota));"
(("i") ("j")))
)))
```

```
(def-theorem negated-defined-iota-expression-elimination
"forall(p:[ind_1,prop],
not(#(iota(i:ind_1,p(i))))
iff
(forall(i:ind_1,
not(p(i)))
or
forsome(i,j:ind_1, p(i) and p(j) and not(i=j))))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(p:[ind_1,prop],not(#(iota(i:ind_1,p(i)))));")
(eliminate-iota 0)
auto-instantiate-existential
(backchain "with(p:prop, forall(i,j:ind_1,p))")
simplify
(apply-macete-with-minor-premises
negated-defined-iota-expression-elimination-1)
(apply-macete-with-minor-premises
negated-defined-iota-expression-elimination-2)
auto-instantiate-existential
)))
```

```
(def-theorem left-iota-expression-equation-elimination
"forall(a:ind_1,p:[ind_1,prop],
iota(i:ind_1,p(i)) = a iff (p(a) and forall(b:ind_1, p(b) implies b=a)))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "a" "iota(i:ind_1,p(i))" (0))
(apply-macete-with-minor-premises
defined-iota-expression-satisfiability)
(apply-macete-with-minor-premises
defined-iota-expression-iota-free-uniqueness)
auto-instantiate-existential
(eliminate-iota 0)
auto-instantiate-existential
)))
```

```
(def-theorem right-iota-expression-equation-elimination
"forall(a:ind_1,p:[ind_1,prop],
a = iota(i:ind_1,p(i)) iff (p(a) and forall(b:ind_1, p(b) implies b=a)))"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "a" "iota(i:ind_1,p(i))" (0))
(apply-macete-with-minor-premises
defined-iota-expression-satisfiability)
(apply-macete-with-minor-premises
defined-iota-expression-iota-free-uniqueness)
auto-instantiate-existential
(eliminate-iota 0)
auto-instantiate-existential
)))
```

```(def-schematic-macete tr%abstraction-for-iota-body
"with(body:prop,
iota(i:ind_1,body) == iota(i:ind_1,lambda(i:ind_1,body)(i)))"
null
transportable
(theory pure-generic-theory-1))
```

```
(def-compound-macete iota-abstraction-macete
(sound
tr%abstraction-for-iota-body
beta-reduce-unstoppably
beta-reduce-unstoppably))
```

```(def-schematic-macete tr%abstraction-for-forsome-body
"with(body:prop,
forsome(i:ind_1,body) iff forsome(i:ind_1,lambda(i:ind_1,body)(i)))"
null
transportable
(theory pure-generic-theory-1))
```

```
(def-compound-macete eliminate-iota-macete
(sequential
iota-abstraction-macete
(series
tr%defined-iota-expression-elimination
tr%negated-defined-iota-expression-elimination
tr%left-iota-expression-equation-elimination
tr%right-iota-expression-equation-elimination)
beta-reduce))
```

```
(def-compound-macete eliminate-forsome-macete
(sequential
(sound
tr%abstraction-for-forsome-body
beta-reduce-unstoppably
beta-reduce-unstoppably)
tr%defined-iota-expression-existence
beta-reduce))
```