[STATEMENT]
lemma norm_pre_pure_rule2:
  "\<lbrakk> b \<Longrightarrow> <emp> f <Q> \<rbrakk> \<Longrightarrow> <\<up>b> f <Q>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<Longrightarrow> <emp> f <Q>) \<Longrightarrow> <\<up> b> f <Q>
[PROOF STEP]
by simp