[STATEMENT]
lemma step_eps_dest: "step_eps bs q q' \<Longrightarrow> q \<in> SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps bs q q' \<Longrightarrow> q \<in> SQ
[PROOF STEP]
by (auto simp add: step_eps_def)