```
(def-quasi-constructor countable%cover
"lambda(v:[zz,sets[ind_1]],a:sets[ind_1],forall(x:ind_1,x in a implies forsome(n:zz,x in v(n))))"
(fixed-theories h-o-real-arithmetic)
(language generic-theory-2))
```

```
(def-quasi-constructor finite%cover
"lambda(v:[zz,sets[ind_1]],a:sets[ind_1],forsome(m:zz,forall(x:ind_1,x in a implies forsome(n:zz,-m<=n and n<=m and x in v(n)))))"
(fixed-theories  h-o-real-arithmetic)
(language generic-theory-2))
```

```
(def-theorem inverse-image-of-covers
"forall(v:[zz,sets[ind_2]],a:sets[ind_1],f:[ind_1,ind_2],total_q(f,[ind_1,ind_2])
implies
countable%cover(v,image(f,a))
iff
countable%cover(lambda(k:zz,if(#(v(k)), inv_image(f,v(k)), ?sets[ind_1])),a))"
(usages transportable-macete)
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
insistent-direct-inference
direct-and-antecedent-inference-strategy
beta-reduce-repeatedly
(instantiate-universal-antecedent
"with(v:[zz,sets[ind_2]],f:sets[ind_2],countable%cover{v,f});"
("f(x_\$0)"))
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
simplify-insistently
(instantiate-existential ("x_\$0")))
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 1 0)")
(instantiate-existential ("n_\$1"))
simplify))
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 1)")
insistent-direct-inference
direct-and-antecedent-inference-strategy
(contrapose "with(x_\$0:ind_2,f:sets[ind_2],x_\$0 in f);")
simplify-insistently
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,forall(n_\$0:zz,p));")
(instantiate-universal-antecedent
"with(f:[zz,sets[ind_1]],a:sets[ind_1],countable%cover{f,a});"
("x"))
(contrapose "with(x:ind_1,n_\$0:zz,f:[zz,sets[ind_1]],x in f(n_\$0));")
beta-reduce-repeatedly
(contrapose "with(p:prop,forall(n_\$0:zz,p));")
(instantiate-existential ("n_\$0"))
(contrapose "with(x:ind_1,f:sets[ind_1],p:prop,x in if(p, f, f));")
(raise-conditional (0))
(contrapose "with(p:prop,not(p));")
(antecedent-inference "with(p:prop,if_form(p, p, p));")
(contrapose "with(x:ind_1,
x
in inv_image{with(f:[ind_1,ind_2],f),
with(f:sets[ind_2],f)});")
simplify)
)
))
```

```
(def-theorem inverse-image-of-finite-covers
"forall(v:[zz,sets[ind_2]],a:sets[ind_1],f:[ind_1,ind_2],total_q(f,[ind_1,ind_2])
implies
finite%cover(v,image(f,a))
iff
finite%cover(lambda(k:zz,if(#(v(k)), inv_image(f,v(k)), ?sets [ind_1])),a))"
(usages transportable-macete)
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 0
0)")
(instantiate-existential ("m_\$0"))
(instantiate-universal-antecedent "with(p:prop,forall(x_\$0:ind_2,p));"
("f(x_\$0)"))
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
simplify-insistently
(instantiate-existential ("x_\$0")))
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 1 0 0)")
(instantiate-existential ("n_\$1"))
beta-reduce-repeatedly
simplify-insistently))
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 1
0)")
(instantiate-existential ("m_\$0"))
(contrapose "with(x_\$0:ind_2,f:sets[ind_2],x_\$0 in f);")
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(x_\$0:ind_1,p implies p));"
("x"))
(beta-reduce-antecedent "with(x:ind_1,v:sets[ind_1],  x in v)")
(instantiate-universal-antecedent "with(p:prop,forall(n_\$0:zz,p));"
("n_\$0"))
(contrapose "with(p:prop,not(p));")
(backchain "with(i,x_\$0:ind_2,x_\$0=i);")
(contrapose "with(x:ind_1,f:sets[ind_1],p:prop,x in if(p, f, f));")
(raise-conditional (0))
(contrapose "with(p:prop,not(p));")
(antecedent-inference "with(p:prop,if_form(p, p, p));")
(contrapose "with(x:ind_1,
x
in inv_image{with(f:[ind_1,ind_2],f),
with(f:sets[ind_2],f)});")
simplify)
)))
```

```
(def-compound-macete covers-direct-image-to-inverse-image-conversion-macete
(repeat
tr%inverse-image-of-finite-covers
tr%inverse-image-of-covers))
```