Nuprl - Pf surj_is_inj 1 2 1 1 1 2 1 2 1

1. n:
2. f: nn
3. a1: n
4. a2: n
5. f(a1) = f(a2)
6. a1 = a2
7. b: (n+1)
8. b = n (n+1)
9. a: n
10. f(a) = b n

a:n. if a2=a n else f(a) fi = b (n+1)

By: Decide (a = a2)

Generated subgoals:

1 11. a = a2
a:n. if a2=a n else f(a) fi = b (n+1)

2 11. a = a2
a:n. if a2=a n else f(a) fi = b (n+1)

About:

1	11. `a = a2` `a:n. if a2=a n else f(a) fi = b (n+1)`
2	11. `a = a2` `a:n. if a2=a n else f(a) fi = b (n+1)`