PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj 1
1. n:
2. f: nn
3. Surj(n; n; f)
4. a1: n
5. a2: n
6. f(a1) = f(a2)

a1 = a2
By: Decide (a1 = a2)
Generated subgoals:

17. a1 = a2
a1 = a2
27. a1 = a2
a1 = a2

About:
equalnatural_numberfunctionapply