proposition: Lemma myexistsb_prop_exits {A} (P : A -> Prop) (l : list A) : myexistsb_prop P l <-> Exists P l.
proof: Proof. funelim (myexistsb_prop P l). split; intuition auto. inversion H. rewrite H. split; intuition auto. inversion H0. intuition. subst. intuition auto. Qed.
imports: Equations(Equations) Coq.Lists.List