PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
one
one
sym
1
1
1
1
1
1.
T:
Type
2.
S:
Type
3.
f:
T
S
4.
g:
S
T
5.
g o f = Id
6.
f o g = Id
f:(S
T), g:(T
S). InvFuns(S; T; f; g)
By:
Witness g
Generated subgoal:
1
g@0:(T
S). InvFuns(S; T; g; g@0)
About:
g@0:(T
S). InvFuns(S; T; g; g@0)ST f:(ST), g:(TS). InvFuns(S; T; f; g) g@0:(TS). InvFuns(S; T; g; g@0)
