```
(def-constant max%on%set
"lambda(s:sets[ind_1],f:[ind_1,rr],
iota(r:rr,
forsome(x:ind_1, x in s and r = f(x))
and
forall(x:ind_1, x in s implies (not(#(f(x))) or f(x) <= r))))"
(theory generic-theory-1))
```

```
(def-theorem max%on%set-bigger-than-members
"forall(s:sets[ind_1],f:[ind_1,rr],x:ind_1,
x in s
and
#(f(x))
and
#(max%on%set(s,f))
implies
f(x) <= max%on%set(s,f))"
(theory generic-theory-1)
(proof
(
direct-and-antecedent-inference-strategy
(incorporate-antecedent
"with(f:[ind_1,rr],s:sets[ind_1],#(max%on%set(s,f)));")
(unfold-single-defined-constant-globally max%on%set)
direct-inference
(eliminate-defined-iota-expression 0 w)
(backchain "with(p:prop,p and p);")
direct-inference
)))
```

```
(def-theorem disj-commutativity
"forall(a,b:sets[uu], a disj b iff b disj a)"
(theory indicators)
(usages transportable-macete)
(proof
(
insistent-direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(b,a:sets[uu],a disj b);" ("x"))
(instantiate-universal-antecedent "with(a,b:sets[uu],b disj a);" ("x"))
)))
```

```
(def-theorem union-disjointness-left
"forall(a,b,c:sets[uu],
(a union b) disj c
iff
(a disj c and b disj c))"
(theory indicators)
(usages transportable-macete)
(proof
(
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"`direct-and-antecedent-inference-strategy' at (0 0)")
insistent-direct-inference
(instantiate-universal-antecedent "with(p:prop,p);" ("x"))
simplify
simplify)
(block
(script-comment
"`direct-and-antecedent-inference-strategy' at (0 1)")
insistent-direct-inference
(instantiate-universal-antecedent
"with(p:prop,forall(x_\$0:uu,p and p or not(p)));"
("x"))
simplify
simplify)
(instantiate-universal-antecedent
"with(c,a:sets[uu],a disj c);" ("x_\$0"))
(instantiate-universal-antecedent
"with(c,b:sets[uu],b disj c);" ("x_\$0"))
)))
```

```
(def-theorem union-disjointness-right
"forall(a,b,c:sets[uu],
a disj (b union c)
iff
(a disj b and a disj c))"
(theory indicators)
(usages transportable-macete)
(proof
(
(force-substitution "a disj b union c" "(b union c) disj a" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises union-disjointness-left)
(apply-macete-locally
disj-commutativity (0) "(b disj a and c disj a)"))
(block
(script-comment "`force-substitution' at (1)")
(move-to-ancestor 1)
(apply-macete-locally
disj-commutativity (0) "a disj b union c"))
)))
```