PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one sym 1 1 1 1 1 1
1. T: Type
2. S: Type
3. f: TS
4. g: ST
5. g o f = Id
6. f o g = Id

g@0:(TS). InvFuns(S; T; g; g@0)
By: Witness f
Generated subgoal:

1 InvFuns(S; T; g; f)

About:
existsfunctionuniverseequal