qed.
lemma in_list_filter_to_p_true : \forall l,x,p.
in_list nat x (filter nat l p) \to p x = true.
intros 3;elim l
[simplify in H;elim (not_in_list_nil ? ? H)
qed.
lemma in_list_filter_to_p_true : \forall l,x,p.
in_list nat x (filter nat l p) \to p x = true.
intros 3;elim l
[simplify in H;elim (not_in_list_nil ? ? H)