At: auto2 lemma 6 1 1 1 1 1 2 1 1 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. Surj(n; T; f)
7. 
t:T. Dec(R(t))
8. x: (n-1)
9. f(x) = f(n-1)
10. f(x) = f(n-1) 
x = n-1 
n
False
By: Analyze 10
Generated subgoals:None
About:
