Nuprl - Pf surj_is_inj 1 2 1 1 1

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

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

By: Reduce 0 THEN Decide (b = n)

Generated subgoals:

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

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

About:

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