DEFINITION f_equal()
TYPE =
       ∀A:Set.∀B:Set.∀f:A→B.∀x:A.∀y:A.(eq A x y)→(eq B (f x) (f y))
BODY =
Show proof