Level: Lib Thy Top: 1 1
Hypotheses:

  1. n :

  2. f : n n

  3. Surj(n;n;f)

  4. a1 : n

  5. a2 : n

  6. f a1 = f a2

  7. a1 = a2

Conclusion:

a1 = a2

Applied Tactic: Auto
Generated subgoals:

None