1 |
7. f : A A'
8. g : A' A
9. F : x:A B(x) B'(f(x))
10. G : x:A B'(f(x)) B(x)
11. InvFuns(A;A';f;g)
12. u:A. InvFuns(B(u);B'(f(u));F(u);G(u))
13. f1 : A' A''
14. g1 : A'' A'
15. F1 : x':A' B'(x') B''(f1(x'))
16. G1 : x':A' B''(f1(x')) B'(x')
17. InvFuns(A';A'';f1;g1)
18. u:A'. InvFuns(B'(u);B''(f1(u));F1(u);G1(u))
(x:A. B(x)) ~ (x'':A''. B''(x''))
 | 9 steps |