At: auto2 lemma 6 1 1 1 1 1 2 1 1 1 1 1 1 1 2 2 1 1 1 1 1 1 1 3 1
1. n: 
2. 0 < n
3. T: Type
4. R: T
Prop
5. f: 
nT
6. Inj(n; T; f)
7. 
t:T. Dec(R(t))
8. b: T
9. 
b = f(n-1)
10. a: n
11. f(a) = b
12. a1: (n-1)
f(a1) 
{t:T| t = f(n-1) }
By:
Analyze
THEN
Try Auto
Generated subgoal:| 1 | f(a1) = f(n-1) |
About:
