PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1 1 2 2 1 2 1 1 2 1 1
1. T: Type
2. S: Type
3. f: TS
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. a1: {s:S| t:T. f(t) = s }
10. a2: {s:S| t:T. f(t) = s }
11. f@0(a1) = f@0(a2) x,y:T//(f(x) = f(y))

a1 = a2
By: ApFunToHypEquands `x' (f(x)) S 11
Generated subgoals:

112. x: x,y:T//(f(x) = f(y))
f(x) = f(x)
2 x,y:T//(f(x) = f(y)) = x,y:T//(f(x) = f(y))
312. f(f@0(a1)) = f(f@0(a2))
a1 = a2

About:
equalsetexistsapplyuniversefunctionallquotient