PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1 1 1
1. T: Type
2. S: Type
3. f: TS
4. Fin(S)
5. s:S. Dec(t:T. f(t) = s)

EquivRel x,y:T. f(x) = f(y)
By:
Analyze 0
THEN
Analyze 0
THEN
Try Auto
THEN
Analyze 0
Generated subgoals:

None

About:
equalapplyuniversefunctionallexists