[STATEMENT]
lemma ap_tree_extensional:
  "(\<And>x. f \<diamondop> x = g \<diamondop> x) \<Longrightarrow> f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f \<diamondop> x = g \<diamondop> x) \<Longrightarrow> f = g
[PROOF STEP]
by(rule ap_tree_strong_extensional) simp