(def-theorem sb-symmetry-obl 
    "forall(h_0:[nn,sets[ind_2]],h_1:[nn,sets[ind_1]],
          forall(u_0:nn,
              #(if(u_0=0, 
                        dom{g},
                        lambda(dummy_$0:sets[ind_1],
                            if(#(dummy_$0), image{f,dummy_$0}, ?sets[ind_2]))(h_1(u_0-1))))
                  implies 
              if(u_0=0,
                    dom{g},
                    lambda(dummy_$0:sets[ind_1],
                        if(#(dummy_$0), image{f,dummy_$0}, ?sets[ind_2]))(h_1(u_0-1)))=h_0(u_0))
              and 
          forall(u_0:nn,
              #(if(u_0=0,
                        dom{f},
                        lambda(dummy_$1:sets[ind_2],
                            if(#(dummy_$1), image{g,dummy_$1}, ?sets[ind_1]))(h_0(u_0-1))))
                  implies 
              if(u_0=0,
                    dom{f},
                    lambda(dummy_$1:sets[ind_2],
                        if(#(dummy_$1), image{g,dummy_$1}, ?sets[ind_1]))(h_0(u_0-1)))=h_1(u_0))
          implies 
              forall(u_0:nn,#(b%seq(u_0)) implies b%seq(u_0)=h_0(u_0))
                  and 
              forall(u_0:nn,#(a%seq(u_0)) implies a%seq(u_0)=h_1(u_0)))"
    lemma
    (theory schroeder-bernstein-theory)
    (proof
      (
        (assume-theorem 
          schroeder-bernstein-set-functions-strong-minimality_schroeder-bernstein-theory)
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, forall(h_0:[nn,sets[ind_1]],h_1:[nn,sets[ind_2]], p))")
        direct-inference
        auto-instantiate-existential
        (backchain "with(p:prop, forall(h_0:[nn,sets[ind_1]],h_1:[nn,sets[ind_2]], p))")
        direct-inference
        auto-instantiate-existential
        )))

(def-theorem sb->gt2-obl-1 
    "forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1], 
          nonempty_indic_q{a}
            and 
          nonempty_indic_q{b}
            and 
          dom{u}=a
            and 
          dom{v}=b
            and 
          ran{u} subseteq b
            and 
          ran{v} subseteq a
            and 
          injective_on_q{u,a}
            and 
          injective_on_q{v,b}
            implies 
          forall(x_$0:ind_1,
              if_form(x_$0 in a,
                  #(u(x_$0)) implies u(x_$0) in b,
                  not(#(u(x_$0))))))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%element-of-a-subset-is-an-element)
        auto-instantiate-existential
        (apply-macete-with-minor-premises range-domain-membership)
        (apply-macete-with-minor-premises domain-membership-iff-defined)
        (apply-macete-with-minor-premises rev%domain-membership-iff-defined)
        (backchain "with(a:sets[ind_1],u:[ind_1,ind_2],dom{u}=a)")
        )))

(def-theorem sb->gt2-obl-2 
    "forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1], 
          nonempty_indic_q{a}
            and 
          nonempty_indic_q{b}
            and 
          dom{u}=a
            and 
          dom{v}=b
            and 
          ran{u} subseteq b
            and 
          ran{v} subseteq a
            and 
          injective_on_q{u,a}
            and 
          injective_on_q{v,b}
            implies 
          forall(x_$0:ind_2,
              if_form(x_$0 in b,
                  #(v(x_$0)) implies v(x_$0) in a,
                  not(#(v(x_$0))))))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%element-of-a-subset-is-an-element)
        auto-instantiate-existential
        (apply-macete-with-minor-premises tr%range-domain-membership)
        (apply-macete-with-minor-premises tr%domain-membership-iff-defined)
        (apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
        (backchain "with(b:sets[ind_2],v:[ind_2,ind_1],dom{v}=b)")
        )))

(def-theorem sb->gt2-obl-3 
    "forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1], 
          nonempty_indic_q{a}
            and 
          nonempty_indic_q{b}
            and 
          dom{u}=a
            and 
          dom{v}=b
            and 
          ran{u} subseteq b
            and 
          ran{v} subseteq a
            and 
          injective_on_q{u,a}
            and 
          injective_on_q{v,b}
            implies 
          forall(x_0:ind_1,x_0 in a implies #(u(x_0))))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises rev%domain-membership-iff-defined)
        (backchain "with(a:sets[ind_1],u:[ind_1,ind_2],dom{u}=a)")
        )))

(def-theorem sb->gt2-obl-4 
    "forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1], 
          nonempty_indic_q{a}
            and 
          nonempty_indic_q{b}
            and 
          dom{u}=a
            and 
          dom{v}=b
            and 
          ran{u} subseteq b
            and 
          ran{v} subseteq a
            and 
          injective_on_q{u,a}
            and 
          injective_on_q{v,b}
            implies 
          forall(x_0:ind_2,x_0 in b implies #(v(x_0))))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
        (backchain "with(b:sets[ind_2],v:[ind_2,ind_1],dom{v}=b)")
        )))

(def-theorem sb->gt2-obl-5 
    "forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1], 
          nonempty_indic_q{a}
            and 
          nonempty_indic_q{b}
            and 
          dom{u}=a
            and 
          dom{v}=b
            and 
          ran{u} subseteq b
            and 
          ran{v} subseteq a
            and 
          injective_on_q{u,a}
            and 
          injective_on_q{v,b}
            implies 
          forall(x_1,x_2:ind_1,
              x_1 in a and x_2 in a
                implies 
              (u(x_1)=u(x_2) implies x_1=x_2)))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(u:[ind_1,ind_2],a:sets[ind_1],injective_on_q{u,a})")
        direct-inference
        )))

(def-theorem sb->gt2-obl-6 
    "forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1], 
          nonempty_indic_q{a}
            and 
          nonempty_indic_q{b}
            and 
          dom{u}=a
            and 
          dom{v}=b
            and 
          ran{u} subseteq b
            and 
          ran{v} subseteq a
            and 
          injective_on_q{u,a}
            and 
          injective_on_q{v,b}
            implies 
          forall(x_1,x_2:ind_2,
              x_1 in b and x_2 in b
                implies 
              (v(x_1)=v(x_2) implies x_1=x_2)))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(v:[ind_2,ind_1],b:sets[ind_2],injective_on_q{v,b})")
        direct-inference
        )))