PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj

n:, f:(nn). Surj(n; n; f) Inj(n; n; f)
By:
Unfold `inject` 0
THEN
UnivCD
Generated subgoal:

11. n:
2. f: nn
3. Surj(n; n; f)
4. a1: n
5. a2: n
6. f(a1) = f(a2)
a1 = a2

About:
allfunctionnatural_numberimpliesequal