PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dist func 1 1 1 1 1
1. St: Type
2. n:
3. f: nSt
4. g: Stn
5. InvFuns(n; St; f; g)

x,y:St. (x,y. g(x)=g(y))(x,y) x = y
By:
Reduce 0
THEN
RepD
Generated subgoal:

16. x: St
7. y: St
8. g(x)=g(y)
x = y

About:
allimpliesassertapplylambda
equaluniversefunctionnatural_number