At: prod fin is fin 1 2 6 1 1 1 1 9 1
1. T: Type
2. t: T
3. n: 
4. f: n
T
5. 
a1,a2:n. f(a1) = f(a2) 
a1 = a2
6. Surj(n; T; f)
7. n > 0
8. a1: (n
n)
9. a2: (nn)
10. f(a1 
n) = f(a2 n)
11. f(a1 rem n) = f(a2 rem n)
12. (a1 n) = (a2 n) 
n
13. (a1 rem n) = (a2 rem n) n
14. a1 = (a1 n)n+(a1 rem n)
15. a2 = (a2 n)n+(a2 rem n)
a1 = a2
By: Analyze
Generated subgoals:None
About:
