At: auto2 lemma 6 1 1 1 1 1 2 1 1 1 1 1 1 1 2 1 1 1 1 1 1
1. n: 
2. 0 < n
3. T: Type
4. R: T
Prop
5. f: 
nT
6. 
a1,a2:n. f(a1) = f(a2) 
a1 = a2
7. Surj(n; T; f)
8. t:T. Dec(R(t))
9. a1: (n-1)
10. a2: (n-1)
11. f(a1) = f(a2) 
{t:T| 
t = f(n-1) }
f(a1) = f(a2)
By: Analyze 11
Generated subgoals:None
About:
