At: auto2 lemma 6 1 1 1 1 1 2 1 1 1 1 1 2 2 1 2 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. 
a1,a2:n. f(a1) = f(a2) 
a1 = a2
7. 
R(f(n-1))
8. t: T
9. R(t)
10. a: n
11. f(a) = f(n-1)
12. a = n-1 
n
13. t = f(n-1)
False
By:
InstHyp [a;n-1] 6
THEN
Try Auto
Generated subgoals:None
About:
