(def-language pure-generic-language-1-with-1-subsort
    (embedded-language pure-generic-language-1)
    (sorts (uu_1 ind_1)))

(def-language pure-generic-language-2-with-2-subsorts
    (embedded-language pure-generic-language-2)
    (sorts (uu_1 ind_1) (uu_2 ind_2)))

(def-theory pure-generic-theory-1-with-1-subsort 
    (language pure-generic-language-1-with-1-subsort)
    (component-theories pure-generic-theory-1))

(def-theory pure-generic-theory-2-with-1-subsort 
    (language pure-generic-language-1-with-1-subsort)
    (component-theories pure-generic-theory-2))

(def-theory pure-generic-theory-2-with-2-subsorts 
    (language pure-generic-language-2-with-2-subsorts)
    (component-theories pure-generic-theory-2))

(def-theory pure-generic-theory-3-with-2-subsorts 
    (language pure-generic-language-2-with-2-subsorts)
    (component-theories pure-generic-theory-3))

(def-theorem surjective-inverse-with-subsort 
    "forall(a:sets[ind_1],f:[uu_1,ind_2],
          injective_on_q(f,a) and dom(f)=a 
            implies 
          surjective_on_q{inverse{f},ran{f},a})"
    (theory pure-generic-theory-2-with-1-subsort)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        insistent-direct-and-antecedent-inference-strategy
        (block 
          (script-comment 
            "`insistent-direct-and-antecedent-inference-strategy' at (0)")
          (apply-macete-with-minor-premises tr%dom-of-inverse)
          (apply-macete-with-minor-premises tr%injective-iff-injective-on-domain)
          simplify)
        (block 
          (script-comment 
            "`insistent-direct-and-antecedent-inference-strategy' at (1)")
          (backchain-backwards "with(a:sets[ind_1],f:sets[uu_1],f=a);")
          extensionality
          direct-inference
          (case-split ("#(x_0,uu_1)"))
          (block 
            (script-comment "`case-split' at (1)")
            beta-reduce-repeatedly
            (raise-conditional (1))
            simplify
            direct-and-antecedent-inference-strategy
            (block 
              (script-comment 
	"`direct-and-antecedent-inference-strategy' at (0 0 0 0)")
              (cut-with-single-formula "x_0=iota(y:uu_1,f(y)=x_$4) and x_0=x_0")
              (incorporate-antecedent "with(u:uu_1,x_0:ind_1,x_0=u);")
              (eliminate-defined-iota-expression 0 w)
              simplify)
            (block 
              (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 1)")
              (instantiate-existential ("f(x_0)"))
              (eliminate-iota 0)
              (instantiate-existential ("x_0"))
              (instantiate-universal-antecedent 
	"with(f:[uu_1,ind_2],a:sets[ind_1],injective_on_q{f,a});"
	("z%iota_$0" "x_0"))
              (block 
	(script-comment "`instantiate-universal-antecedent' at (0 0 0 0)")
	(contrapose "with(p:prop,not(p));")
	(backchain-backwards "with(a:sets[ind_1],f:sets[uu_1],f=a);")
	beta-reduce-insistently
	simplify)
              (block 
	(script-comment "`instantiate-universal-antecedent' at (0 0 0 1)")
	(contrapose "with(p:prop,not(p));")
	(backchain-backwards "with(a:sets[ind_1],f:sets[uu_1],f=a);")
	beta-reduce-insistently
	simplify)))
          (block 
            (script-comment "`case-split' at (2)")
            insistent-direct-and-antecedent-inference-strategy
            (contrapose "with(p:prop,not(p));")
            (incorporate-antecedent "with(x_0:ind_1,f:sets[ind_1],x_0 in f);")
            beta-reduce-insistently
            simplify
            direct-and-antecedent-inference-strategy))
        )))