[STATEMENT]
lemma pure_eq_iff:     
  "(\<forall>h' x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h' \<longrightarrow> h = h') \<longleftrightarrow> pure f h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h' x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h' \<longrightarrow> h = h') = pure f h
[PROOF STEP]
by(auto simp add: pure_def)