At:
fun-graph-rel-graph
3
1
1
1
1
1.
A: Type
2.
B: Type
3.
f: A
BA
4.
a:A, b1,b2:B. f(a,b1) = f(a,b2) 
b1 = b2
5.
a,a':A. Dec(
b:B. a' = f(a,b))
6.
a3: A
7.
a4: B
8.
a5: A
9.
a6: B
10.
b: B
11.
f(a3,a4) = f(a3,b)
12.
a3 = a5
13.
f(a5,a4) = f(a5,a6)
a4 = a6
By:
FwdThru 4 [-1]
Generated subgoals:
None
About:
