[STATEMENT]
lemma all_final_exceptD:
  "\<lbrakk> all_final_except s Ts; not_final_thread s t \<rbrakk> \<Longrightarrow> t \<in> Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>all_final_except s Ts; not_final_thread s t\<rbrakk> \<Longrightarrow> t \<in> Ts
[PROOF STEP]
by(auto simp add: all_final_except_def)