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:
n
St
4.
g:
St
n
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)
2
10.
(f o g)(x) = (f o g)(y)
x = y
About: