proposition: Lemma ext_in_filter : forall (f g : A -> bool) (l : list A), filter f l = filter g l -> (forall a, In a l -> f a = g a).
proof: Proof. intros f g l. induction l as [| a l IHl]; [easy|cbn]. intros H. assert (Ha : f a = g a). - pose proof (Hf := proj1 (filter_In f a l)). pose proof (Hg := proj1 (filter_In g a l)). destruct (f a), (g a); [reflexivity| | |reflexivity]. + symmetry. apply Hg. rewrite <- H. now left. + apply Hf. rewrite H. now left. - intros b [<-|Hbl]; [assumption|]. apply IHl; [|assumption]. destruct (f a), (g a); congruence. Qed.
imports: PeanoNat