proposition: Lemma filter_ext_in : forall (f g : A -> bool) (l : list A), (forall a, In a l -> f a = g a) -> filter f l = filter g l.
proof: Proof. intros f g l. induction l as [| a l IHl]; [easy|cbn]. intros H. rewrite (H a) by (now left). destruct (g a); [f_equal|]; apply IHl; intros; apply H; now right. Qed.
imports: PeanoNat