At:
fun-graph-rel-graph
3
2
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.
b1: A
7.
b2: A
8.
b1@0: B
9.
b2 = f(b1,b1@0)
< b1,f(b1,b1@0) > = < b1,b2 >
By:
Analyze
Generated subgoals:
None
About:
