At: inv of fin is fin 1 1 2 2 1 2 1 1 2 2 1 2 3 1 2 1 2
1. T: Type
2. S: Type
3. f: T
S
4. Fin(S)
5. 
s:S. Dec(
t:T. f(t) = s)
6. EquivRel x,y:T. f(x) = f(y)
7. f@0: {s:S| t:T. f(t) = s }T
8. s:{s:S| t:T. f(t) = s }. f(f@0(s)) = s
9. b: x,y:T//(f(x) = f(y))
10. t: T
f(t) = f(b) 
Prop
By: Analyze
Generated subgoals:| 1 | S Type |
| 2 | f(t) S |
| 3 | f(b) S |
About:
