[STATEMENT]
lemma ttree_restr_possible2: "possible (ttree_restr S t') x \<Longrightarrow> x \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. possible (ttree_restr S t') x \<Longrightarrow> x \<in> S
[PROOF STEP]
by transfer (auto, metis filter_eq_Cons_iff)