[STATEMENT]
lemma ent_pure_post_iff_sng[simp]: 
  "(P \<Longrightarrow>\<^sub>A \<up>b) \<longleftrightarrow> ((\<forall>h. h\<Turnstile>P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))
[PROOF STEP]
using ent_pure_post_iff[where Q=emp]
[PROOF STATE]
proof (prove)
using this:
(?P \<Longrightarrow>\<^sub>A emp * \<up> ?b) = ((\<forall>h. h \<Turnstile> ?P \<longrightarrow> ?b) \<and> (?P \<Longrightarrow>\<^sub>A emp))

goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))
[PROOF STEP]
by simp