At:
compose-biject
2
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.
b: C
11.
a: B
12.
g(a) = b
13.
a@0: A
14.
f(a@0) = a
g(f(a@0)) = b
By:
Obvious
Generated subgoals:
None
About:
