PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dist func 1 1 1 1 1 1 1 2 1

1. St: Type
2. n:
3. f: nSt
4. g: Stn
5. g o f = Id
6. f o g = Id
7. x: St
8. y: St
9. f(g(x)) = f(g(y))

x = y

By: Assert ((f o g)(x) = (f o g)(y))

Generated subgoals:

1 (f o g)(x) = (f o g)(y)
210. (f o g)(x) = (f o g)(y)
x = y


About:
equalapplyuniversefunctionnatural_number