At: one one preser fin 1 1 1 1 1 1 2 1 1 1 1 1 1 1
1. T: Type
2. S: Type
3. n: 
4. f: n
T
5. Inj(n; T; f)
6. f1: TS
7. g: ST
8. g o f1 = Id
9. f1 o g = Id
10. b: S
11. a: n
12. f(a) = g(b)
f1(g(b)) = b
By: RWH add_composeC 0
Generated subgoal:| 1 | (f1 o g)(b) = b |
About:
