Level: Lib Thy Top: 1 2
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: Assert h:n (n + 1). Surj(n;(n + 1);h)
Generated subgoals:

1. h:n (n + 1). Surj(n;(n + 1);h)

2. a1 = a2