[STATEMENT]
lemma lconf_empty[iff]: "P,h \<turnstile> Map.empty (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> Map.empty (:\<le>)\<^sub>w E
[PROOF STEP]
by(simp add:lconf_def)