At: bool listify 1 1 1 2 1 1 1
1. T: Type
2. f: T
3. n: 
4. f1: nT
5. Bij(n; T; f1)
6. k: 
7. 0 < k
8. k
n
9. fL: T*
10. 
t:T. mem_f(T;t;fL) 
f(t)
11. i:(k-1). f(f1(i)) mem_f(T;f1(i);fL)
12. f(f1(k-1))
13. t: T
14. f1(k-1) = t 
mem_f(T;t;fL)
f(t)
By: Analyze -1
Generated subgoals:| 1 | 14. f1(k-1) = t
f(t) |
| 2 | 14. mem_f(T;t;fL)
f(t) |
About:
