Level: Lib Thy Top: 1 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:

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

Applied Tactic: (Unfold `inv_funs` 0 THENM Unfold `inv_funs` 9 THENM Unfold `inv_funs` 6 THENM ExRepD ...a)
Generated subgoals:

1. (g1 o g) o (f o f1) = Id{A} (f o f1) o (g1 o g) = Id{C}