1 |
( h.f o h o g1) (A inj B) A' inj B'
 | 3 steps |
2 |
19. ( h.f o h o g1) (A inj B) A' inj B'
( h.g o h o f1) (A' inj B') A inj B
 | 1 step |
3 |
19. ( h.f o h o g1) (A inj B) A' inj B'
20. ( h.g o h o f1) (A' inj B') A inj B
InvFuns(A inj B;A' inj B'; h.f o h o g1; h.g o h o f1)
 | 7 steps |