(def-theorem unary-eta-reduction 
    "forall(f:[ind_1,ind_2], lambda(x:ind_1,f(x))=f);"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        simplify
        )))

(def-theorem domain-membership-iff-defined 
    "forall(x:ind_1,f:[ind_1,ind_2], x in dom(f) iff #(f(x)))"
    reverse
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem range-domain-membership 
    "forall(x:ind_1,f:[ind_1,ind_2], f(x) in ran{f} iff x in dom(f))"
    reverse
    (theory pure-generic-theory-2)
    (usages transportable-macete transportable-rewrite)
    (proof
      (
        simplify-insistently
        direct-and-antecedent-inference-strategy
        simplify-insistently
        (instantiate-existential ("x"))
        )))

(def-theorem membership-in-a-domain 
    "forall(x:ind_1,a:sets[ind_1],f:[ind_1,ind_2], 
          dom{f}=a and #(f(x)) implies x in a)"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (force-substitution "a" "dom{f}" (0))
        (apply-macete-with-minor-premises tr%domain-membership-iff-defined)
        )))

(def-theorem membership-in-a-range 
    "forall(x:ind_1,y:ind_2,b:sets[ind_2],f:[ind_1,ind_2],
          ran{f}=b and y=f(x) implies y in b)"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (force-substitution "b" "ran{f}" (0))
        (force-substitution "y" "f(x)" (0))
        (apply-macete-with-minor-premises tr%range-domain-membership)
        simplify-insistently
        )))

(def-theorem dom-of-an-indicator 
    "forall(a:sets[ind_1], dom{a}=a)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        extensionality
        direct-inference
        simplify-insistently
        (case-split-on-conditionals (0))
        )))

(def-theorem associativity-of-composition 
    "forall(f:[ind_3,ind_4],g:[ind_2,ind_3],h:[ind_1,ind_2], 
          (f oo g) oo h = f oo (g oo h))"
    reverse
    (theory pure-generic-theory-4)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify
        )))

(def-theorem composition-decreases-domain 
    "forall(f:[ind_1,ind_2], g:[ind_2,ind_3], 
          dom{g oo f} subseteq dom{f})"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem composition-decreases-range 
    "forall(f:[ind_1,ind_2], g:[ind_2,ind_3], 
          ran{g oo f} subseteq ran{g})"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        simplify-insistently
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        )))

(def-theorem domain-composition 		 
    "forall(f:[ind_1,ind_2], g:[ind_2,ind_3], 
          ran{f} subseteq dom{g} implies dom{g oo f} = dom{f})"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        simplify-insistently
        direct-and-antecedent-inference-strategy
        extensionality
        direct-and-antecedent-inference-strategy
        simplify
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop,not(p));")
        (instantiate-universal-antecedent "with(p:prop,forall(x_$0:ind_2,p));"
				            ("f(x_0)"))
        (instantiate-universal-antecedent "with(p:prop,forall(x_$1:ind_1,p));" ("x_0")))))

(def-theorem range-composition 		 
    "forall(f:[ind_1,ind_2], g:[ind_2,ind_3], 
          dom{g} subseteq ran{f} implies ran{g oo f} = ran{g})"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
      
        simplify-insistently
        direct-and-antecedent-inference-strategy
        extensionality
        direct-and-antecedent-inference-strategy
        simplify
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
            auto-instantiate-existential)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (1 0)")
            (contrapose "with(p:prop,not(p));")
            (instantiate-universal-antecedent "with(p:prop,forall(x_$0:ind_2,p));"
					("x"))
            (instantiate-existential ("x_$1"))
            simplify))))

(def-theorem injective-composition 
    "forall(f:[ind_1,ind_2], g:[ind_2,ind_3], 
          injective_q{f} and injective_on_q{g,ran{f}} implies injective_q{g oo f})"
    (theory pure-generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        direct-inference
        (backchain "with(f:[ind_1,ind_2],injective_q{f})")
        (backchain 
          "with(g:[ind_2,ind_3],f:[ind_1,ind_2], injective_on_q{g,ran{f}})")
        (incorporate-antecedent "with(x,y:ind_3, x=y)")
        (weaken (0 1))
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("x_$0"))
        (instantiate-existential ("x_$1"))
        simplify
        )))

(def-theorem image-of-domain-is-range 
    "forall(f:[ind_1,ind_2], image{f,dom{f}} = ran{f})"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        direct-inference
        insistent-direct-inference
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("x_$1"))
        insistent-direct-inference
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("x"))
        )))

(def-theorem image-subset-of-range-characterization 
    "forall(s:sets[ind_1],f:[ind_1,ind_2], 
          s subseteq dom{f} implies image{f,s} subseteq ran{f})"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        simplify-insistently
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        )))

(def-theorem image-is-monotone-wrt-subseteq 
    "forall(f:[ind_1,ind_2],a,b:sets[ind_1],
          (a subseteq b) implies (image(f,a) subseteq image(f,b)))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        simplify-insistently
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        (backchain "with(b,a:sets[ind_1],a subseteq b)")
        )))

(def-theorem direct-image-disjointness-conversion 
    "forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
          empty_indic_q(b inters image(f,a)) iff empty_indic_q(inv_image(f,b) inters a))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, forall(x_$0:ind_2,p))")
        auto-instantiate-existential
        (contrapose "with(p:prop, forall(x_$0:ind_1,p))")
        auto-instantiate-existential
        simplify
        )))

(def-theorem direct-image-subset-conversion 	 
    "forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
          total_q(f,[ind_1,ind_2]) 
            implies 
          (image(f,a) subseteq b iff a subseteq inv_image(f,b)))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, forall(x_$0:ind_2,p))")
        auto-instantiate-existential
        (auto-instantiate-universal-antecedent "with(p:prop, forall(x_$0:ind_1,p))")
        simplify
        )))

(def-theorem inverse-image-union-preservation 
    "forall(f:[ind_1,ind_2],a,b:sets[ind_2], 
          inv_image(f,a union b) = inv_image(f,a) union inv_image(f,b))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (contrapose "with(y:ind_2,a:sets[ind_2], y in a)")
        (case-split ("#(f(x_$2))"))
        (apply-macete-with-minor-premises tr%membership-in-union)
        simplify
        simplify
        (apply-macete-with-minor-premises tr%membership-in-union)
        simplify
        (apply-macete-with-minor-premises tr%membership-in-union)
        simplify
        )))

(def-theorem inverse-image-inters-preservation 
    "forall(f:[ind_1,ind_2],a,b:sets[ind_2], 
          inv_image(f,a inters b) = inv_image(f,a) inters inv_image(f,b))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        simplify-insistently
        (apply-macete-with-minor-premises tr%membership-in-intersection)
        )))

(def-theorem meaning-of-inverse-image-membership  
    "forall(f:[ind_1,ind_2],x:ind_1,o:sets[ind_2],
          x in inv_image(f,o) iff f(x) in o)"
  (theory pure-generic-theory-2)
  (usages transportable-macete)
  (proof (simplify-insistently)))

(def-compound-macete direct-image-to-inverse-image-conversion-macete 
    (repeat
      tr%direct-image-disjointness-conversion
      tr%direct-image-subset-conversion
      tr%inverse-image-union-preservation
      tr%inverse-image-inters-preservation))

(def-compound-macete indicator-facts-macete 
    (repeat
      tr%meaning-of-indic-from-pred-element
      tr%meaning-of-inverse-image-membership))

(def-theorem dom-of-id 
    "forall(a:sets[ind_1], dom{id{a}} = a)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify-insistently
        (case-split-on-conditionals (0))
        )))

(def-theorem ran-of-id 
    "forall(a:sets[ind_1], ran{id{a}} = a)"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify-insistently
        (case-split-on-conditionals (0))
        (antecedent-inference "with(p:prop, forsome(x_$1:ind_1,p))")
        (incorporate-antecedent "with(x,y:ind_1, x=y)")
        (case-split-on-conditionals (0))
        (contrapose "with(p:prop, not(p))")
        (instantiate-existential ("x_0"))
        simplify
        )))

(def-theorem id-is-injective-on-dom 
    "forall(a:sets[ind_1], injective_on_q{id{a},a})"
    (theory pure-generic-theory-1)
    (usages transportable-macete)
    (proof
      (
        insistent-direct-inference-strategy
        (antecedent-inference "with(p,q,r:prop, p and q and r)")
        (incorporate-antecedent "with(x,y:ind_1, x = y)")
        simplify-insistently
        )))

(def-theorem composition-with-id-right 
    "forall(f:[ind_1,ind_2], a:sets[ind_1], f oo id{a} = restrict{f,a})"
    (theory pure-generic-theory-2)
    (usages transportable-macete transportable-rewrite)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify
        (case-split-on-conditionals (0)))))

(def-theorem composition-with-id-left 
    "forall(f:[ind_1,ind_2],a:sets[ind_2], 
          id{a} oo f = restrict{f,inv_image{f,a}})"
    (theory pure-generic-theory-2)
    (usages transportable-macete transportable-rewrite)
    (proof
      (
        direct-inference
        extensionality
        direct-inference
        simplify
        (case-split-on-conditionals (0))
        )))

(def-theorem composition-with-total-id-left 
    "forall(f:[ind_1,ind_2],a:sets[ind_2], 
          total_q{a,sets[ind_2]} implies id{a} oo f = f)"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        extensionality
        direct-inference
        (case-split ("#(f(x_0))"))
        simplify
        simplify
        )))

(def-theorem composition-with-total-id-right 
    "forall(f:[ind_1,ind_2], a:sets[ind_1], 
          total_q{a,sets[ind_1]} implies f oo id{a} = f)"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        extensionality
        direct-inference
        (case-split ("#(f(x_0))"))
        simplify
        simplify
        )))

(def-theorem surjective-on-lemma 
    "forall(a:sets[ind_1],b:sets[ind_2],f:[ind_1,ind_2],x:ind_1,
          surjective_on_q(f,a,b) and (x in a) implies (f(x) in b))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (force-substitution "b" "ran{f}" (0))
        (apply-macete-with-minor-premises tr%range-domain-membership)
        simplify
        )))

(def-theorem domain-of-a-bijective-composition 
    "forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],f:[ind_1,ind_2],g:[ind_2,ind_3], 
          bijective_on_q(f,a,b) and bijective_on_q(g,b,c) implies dom(g oo f) = a)"
  (theory pure-generic-theory-3)
  (usages transportable-macete)
  (proof
    (
      direct-and-antecedent-inference-strategy
      (apply-macete-with-minor-premises tr%domain-composition)
      )))

(def-theorem range-of-a-bijective-composition 
    "forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],f:[ind_1,ind_2],g:[ind_2,ind_3], 
          bijective_on_q(f,a,b) and bijective_on_q(g,b,c) implies ran(g oo f) = c)"
  (theory pure-generic-theory-3)
  (usages transportable-macete)
  (proof
    (
      direct-and-antecedent-inference-strategy
      (apply-macete-with-minor-premises tr%range-composition)
      )))

(def-theorem injective-and-surjective-is-total 
    "forall(f:[ind_1,ind_2], 
          injective_q{f} and surjective_q{f} implies total_q{f,[ind_1,ind_2]})"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof (simplify-insistently)))

(def-theorem injective-implies-injective-on 
    "forall(f:[ind_1,ind_2],a:sets[ind_1], 
          injective_q{f} implies injective_on_q{f,a})" 
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        insistent-direct-inference-strategy
        simplify
        )))

(def-theorem injective-iff-injective-on-domain 
    "forall(f:[ind_1,ind_2],a:sets[ind_1], 
          injective_q{f} iff injective_on_q{f,dom{f}})"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises injective-implies-injective-on)
        insistent-direct-inference
        direct-inference
        (backchain "with(f:[ind_1,ind_2],injective_on_q{f,dom{f}});")
        simplify
        )))

(def-theorem range-of-bijection-on-singleton 
    "forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
          bijective_on_q{f,a,b} and forsome(x:ind_1,a=singleton{x}) 
            implies
          forsome(y:ind_2,b=singleton{y}))" 
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forall(y:ind_1, y in a iff y=x)")
        (block 
          (script-comment "`cut-with-single-formula' at (0)")
          (cut-with-single-formula "#(f(x))")
          (block 
            (script-comment "`cut-with-single-formula' at (0)")
            (apply-macete-with-minor-premises tr%singletons-have-a-unique-member)
            (instantiate-existential ("f(x)"))
            (backchain-backwards "with(b:sets[ind_2],f:[ind_1,ind_2],ran{f}=b);")
            beta-reduce-insistently
            simplify
            (apply-macete-with-minor-premises eliminate-iota-macete)
            direct-inference
            (instantiate-existential ("x"))
            (block 
              (script-comment "`direct-inference' at (1)")
              direct-and-antecedent-inference-strategy
              (backchain "with(i,b_$0:ind_2,b_$0=i);")
              (instantiate-universal-antecedent "with(p:prop,forall(y:ind_1,p));"
					  ("x_$1"))
              (contrapose "with(x_$1:ind_1,a:sets[ind_1],not(x_$1 in a));")
              (backchain-backwards "with(a:sets[ind_1],f:[ind_1,ind_2],dom{f}=a);")
              (apply-macete-with-minor-premises domain-membership-iff-defined)))
          (block 
            (script-comment "`cut-with-single-formula' at (1)")
            (apply-macete-with-minor-premises rev%domain-membership-iff-defined)
            (force-substitution "dom{f}" "singleton{x}" (0))
            (weaken (0 1 2 3 4))
            simplify-insistently))
        (block 
          (script-comment "`cut-with-single-formula' at (1)")
          (backchain "with(x:ind_1,a:sets[ind_1],a=singleton{x});")
          (weaken (0 1 2 3))
          simplify-insistently)
        )))

(def-theorem restricted-to-range-composition-lemma 
    "forall(phi:[ind_1,ind_2],f:[ind_2,ind_3],
          f oo phi==(restrict{f,ran{phi}}) oo phi)"
    (theory generic-theory-3)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        simplify-insistently
        extensionality
        direct-and-antecedent-inference-strategy
        (case-split ("#(phi(x_0))"))
        simplify
        (cut-with-single-formula "forsome(x_$1:ind_1,phi(x_0)=phi(x_$1))")
        simplify
        (instantiate-existential ("x_0"))
        simplify
        )))

(def-theorem domain-of-a-restriction 
    "forall(phi:[ind_1,ind_2], s:sets[ind_1], s subseteq dom{phi} implies
                                                          s=dom{restrict{phi,s}})"
    (theory generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        direct-inference
        (apply-macete-with-minor-premises indicator-facts-macete)
        beta-reduce-repeatedly
        simplify
        (apply-macete-with-minor-premises rev%domain-membership-iff-defined)
        (backchain "with(phi:[ind_1,ind_2],s:sets[ind_1],s subseteq dom{phi});")
        insistent-direct-inference
        (apply-macete-with-minor-premises indicator-facts-macete)
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        )))

(def-theorem image-of-a-restriction 
    "forall(phi:[ind_1,ind_2], s:sets[ind_1],image{restrict{phi,s},s}=image{phi,s})"
    (theory generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        (apply-macete-with-minor-premises indicator-facts-macete)
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("x_$1"))
        (contrapose "with(phi:[ind_1,ind_2],x_$1:ind_1,s:sets[ind_1],x_$2:ind_2,
    x_$2=if(x_$1 in s, phi(x_$1), ?ind_2));")
        simplify
        insistent-direct-inference
        (apply-macete-with-minor-premises indicator-facts-macete)
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        simplify
        )))

(def-theorem injectivity-of-a-restriction 
    "forall(phi:[ind_1,ind_2], s:sets[ind_1],injective_q{phi} 
                            implies injective_q{restrict{phi,s}})"
    (theory generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        
        insistent-direct-inference-strategy
        (backchain "with(phi:[ind_1,ind_2],injective_q{phi});")
        (case-split ("x_1 in s " "x_2 in s"))
        (contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
    restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
        simplify
        (contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
    restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
        simplify
        (contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
    restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
        simplify
        (contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
    restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
        simplify
        )))