PrintForm Definitions relation autom Sections AutomataTheory Doc

At: one one corr tran 1 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)

InvFuns(A; C; f o f1; g1 o g)
By:
Unfold `inv_funs` 0
THEN
Unfold `inv_funs` 9
THEN
Unfold `inv_funs` 6
THEN
ExRepD
Generated subgoal:

16. g1 o f1 = Id
7. f1 o g1 = Id
8. f: BC
9. g: CB
10. g o f = Id
11. f o g = Id
g1 o g o f o f1 = Id & f o f1 o g1 o g = Id

About:
universefunctionandequal