At: one one corr tran 1 1 1 2 1
1. A: Type
2. B: Type
3. C: Type
4. f1: A
B
5. g1: BA
6. 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
12. x: C
f((f1 o g1)(g(x))) = x
By:
HypSubst 7 0
THEN
Reduce 0
Generated subgoal:| 1 | f(g(x)) = x |
About:
