[STATEMENT]
lemma bad_guards:
  "\<exists>i. can_take_transition t1 i r \<and> \<not> can_take_transition t2 i r \<Longrightarrow>
   \<not> subsumes t2 r t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. can_take_transition t1 i r \<and> \<not> can_take_transition t2 i r \<Longrightarrow> \<not> subsumes t2 r t1
[PROOF STEP]
by (simp add: subsumes_def)