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