[STATEMENT]
lemma fun_of_simp [simp]: "fun_of S x y = ((x,y) \<in> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun_of S x y = ((x, y) \<in> S)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun_of S x y = ((x, y) \<in> S)
[PROOF STEP]
by (simp add: fun_of_def)