proposition: Lemma existsb_exists : forall l, existsb l = true <-> exists x, In x l /\ f x = true.
proof: Proof. intro l; induction l as [ | a m IH ]; split; simpl. - easy. - intros [x [[]]]. - destruct (f a) eqn:Ha. + intros _. exists a. tauto. + intros [x [? ?]] %IH. exists x. tauto. - intros [ x [ [ Hax | Hxm ] Hfx ] ]. + now rewrite Hax, Hfx. + destruct IH as [ _ -> ]; eauto with bool. Qed.
imports: PeanoNat