proposition: Lemma filter_snoc : forall T f (l : list T) x, filter f (snoc l x) = if f x then snoc (filter f l) x else filter f l.
proof: Proof. induction l; simpl; sp. destruct (f a); simpl; rewrite IHl; destruct (f x); sp. Qed.
imports: UsefulTypes bin_rels Omega