Level: Lib Thy Top: 1
Hypotheses:

  1. A :

  2. B :

  3. C :

  4. f1 : A B

  5. g1 : B A

  6. InvFuns(A;B;f1;g1)

  7. f : B C

  8. g : C B

  9. InvFuns(B;C;f;g)

Conclusion:

f:A C. g:C A. InvFuns(A;C;f;g)

Applied Tactic: (InstConcl [f o f1;g1 o g] ...a)
Generated subgoals:

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