PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj 1 2 2 1 1 1 1 2 1 1
1. n:
2. f: nn
3. Surj(n; n; f)
4. a1: n
5. a2: n
6. f(a1) = f(a2)
7. a1 = a2
8. h: n(n+1)
9. b:(n+1). a:n. h(a) = b
10. f1: (n+1)n
11. b:(n+1). h(f1(b)) = b
12. n = 0
13. i: (n+1)
14. j: i
15. f1(i) = f1(j)

a1 = a2
By: ApFunToHypEquands `z' (h(z)) (n+1) 15
Generated subgoal:

116. h(f1(i)) = h(f1(j))
a1 = a2

About:
equalnatural_numberapplyaddfunctionallexistsint