[STATEMENT]
lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t k = Some x; C k x\<rbrakk> \<Longrightarrow> filter_tab C t k = Some x
[PROOF STEP]
by (simp add: filter_tab_def)