At:
fun-graph-rel-graph
1
1.
A: Type
2.
B: Type
3.
f: A
B
A
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.
p: A
B
< 1of(p),f(1of(p),2of(p)) >
{p:(A
A)|
b:B. 2of(p) = f(1of(p),b)
A }
By:
Analyze -1
THEN
Analyze
THEN
Reduce 0
THEN
InstConcl [p2]
Generated subgoals:
None
About: