At: surj is inj 1 2 1 1 1 2 1 2 1 2
1. n: 
2. f: n
n
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
11. a = a2
a:n. if a2=
a
n else f(a) fi = b (n+1)
By:
Witness a
THEN
SplitOnConclITE
Generated subgoals:None
About:
