(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))