PrintForm Definitions relation autom Sections AutomataTheory Doc

At: one one corr tran 1
1. A: Type
2. B: Type
3. C: Type
4. f1: AB
5. g1: BA
6. InvFuns(A; B; f1; g1)
7. f: BC
8. g: CB
9. InvFuns(B; C; f; g)

f:(AC), g:(CA). InvFuns(A; C; f; g)
By: InstConcl [f o f1;g1 o g]
Generated subgoal:

1 InvFuns(A; C; f o f1; g1 o g)

About:
existsfunctionuniverse