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