PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dist func 1 1 1 1 1 1 1 2 1 2
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))
10. (f o g)(x) = (f o g)(y)

x = y
By: RWH (HypC 6) 10
Generated subgoal:

110. Id(x) = Id(y)
x = y

About:
equaluniversefunctionnatural_numberapply