PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dist func 1 1 1 1

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

eq:(StSt). x,y:St. eq(x,y) x = y

By: InstConcl [x,y. g(x)=g(y)]

Generated subgoal:

1 x,y:St. (x,y. g(x)=g(y))(x,y) x = y


About:
existsfunctionboolallimpliesassert
applyequallambdauniversenatural_number