At:
compose-biject
1
1.
A: Type
2.
B: Type
3.
C: Type
4.
f: A
B
5.
g: BC
6.
a1,a2:A. f(a1) = f(a2) 
a1 = a2
7.
b:B. 
a:A. f(a) = b
8.
a1,a2:B. g(a1) = g(a2) a1 = a2
9.
b:C. a:B. g(a) = b
10.
a1: A
11.
a2: A
12.
g(f(a1)) = g(f(a2))
a1 = a2
By:
Obvious
Generated subgoals:
None
About:
