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