(def-theorem schroeder-bernstein-for-types 
    "forall(f:[ind_2,ind_1],g:[ind_1,ind_2], 
                            total_q{g,[ind_1,ind_2]} and 
                            total_q{f,[ind_2,ind_1]} and
                            injective_q{f} and 
                            injective_q{g}
                                implies
                            forsome(h:[ind_1,ind_2], bijective_q{h}))"
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula
          "forsome(z:sets[ind_1], lambda(x:sets[ind_1],image(f,image(g,x)^^)^^)(z)=z)")
        (move-to-sibling 1)
        (apply-macete-with-minor-premises tr%knaster-fixed-point-theorem)
        (apply-macete-with-minor-premises monotonicity-of-sb-functional)
        (block
          (script-comment
            "this proves the lattice of subsets satisfies the conditions of knaster's
  theorem.")
          direct-and-antecedent-inference-strategy
          unfold-defined-constants
          (instantiate-existential ("empty_indic{ind_1}" "indic{x:ind_1,truth}"))
          simplify-insistently
          simplify-insistently)
        (block
          (script-comment "this uses the fixed point property.")
          (antecedent-inference "with(p:prop,forsome(z:sets[ind_1],p));")
          (beta-reduce-antecedent "with(z:sets[ind_1],f:[ind_2,ind_1],g:[ind_1,ind_2],
    lambda(x:sets[ind_1],image{f,image{g,x}^^}^^)(z)=z);")
          (move-to-ancestor 1)
          (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
          simplify-insistently
          direct-and-antecedent-inference-strategy
          (instantiate-existential ("lambda(x:ind_1,if(x in z, g(x), inverse{f}(x)))"))
          insistent-direct-inference-strategy
          beta-reduce-repeatedly)
        (block
          (script-comment "this proves totality")
          (case-split ("x_$1 in z"))
          simplify
          simplify
          (apply-macete-with-minor-premises eliminate-iota-macete)
          (instantiate-universal-antecedent "with(z:sets[ind_1],p:prop,
    forall(x:ind_1,forall(x_$1:ind_2,p) implies x in z));"
				              ("x_$1"))
          (instantiate-existential ("x_$3"))
          (backchain "with(f:[ind_2,ind_1],injective_q{f});"))
        beta-reduce-repeatedly
        (case-split ("forsome(x:ind_1, x in z and y_$1=g(x))"))
        (instantiate-existential ("x"))
        simplify
        (instantiate-existential ("f(y_$1)"))
        (cut-with-single-formula "not(f(y_$1) in z)")
        simplify
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        (backchain "with(f:[ind_2,ind_1],injective_q{f});")
        (contrapose "with(p:prop,not(p));")
        (instantiate-universal-antecedent "with(p:prop,z:sets[ind_1],
    forall(x_$0:ind_1,x_$0 in z implies forall(x_$1:ind_2,p)));"
				            ("f(y_$1)"))
        (backchain "with(p:prop,forall(x_$3:ind_2,p or p));")
        insistent-direct-inference
        beta-reduce-repeatedly
        (case-split ("x_1 in z" "x_2 in z"))
        direct-and-antecedent-inference-strategy
        (backchain "with(g:[ind_1,ind_2],injective_q{g});")
        (simplify-antecedent "with(i:ind_2,i=i);")
        simplify
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(z:sets[ind_1],p:prop,
    forall(x:ind_1,forall(x_$1:ind_2,p) implies x in z));"
				            ("x_2"))
        (instantiate-universal-antecedent "with(p:prop,forall(x_$0:ind_1,p or p));"
				            ("x_1"))
        (simplify-antecedent "with(p:prop,not(p));")
        simplify
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(z:sets[ind_1],p:prop,
    forall(x:ind_1,forall(x_$1:ind_2,p) implies x in z));"
				            ("x_1"))
        (instantiate-universal-antecedent "with(p:prop,forall(x_$0:ind_1,p or p));"
				            ("x_2"))
        (simplify-antecedent "with(p:prop,not(p));")
        simplify
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "injective_q{inverse{f}}")
        (backchain "with(f:[ind_2,ind_1],injective_q{inverse{f}});")
        simplify-insistently
        (apply-macete-with-minor-premises tr%inverse-is-injective)
        )))