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. n: 
2. 0 < n
3. T: Type
4. R: T
Prop
5. f:
n
T
6. Inj(
n; T; f)
7.
R(f(n-1))
8. t: T
9. R(t)
10. a:
n
11. f(a) = t
12.
a = n-1
n
t = f(n-1)
By: Analyze 0
Generated subgoal:| 1 | 13. t = f(n-1) False |
About: