proposition: Lemma In_filter {A} (f : A -> bool) (l : list A) a : In a (filter f l) -> In a l /\ f a = true.
proof: Proof. induction l; simpl. intros []. destruct (f a0) eqn:Heq. simpl. intuition auto. now subst a0. intuition auto. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia) List