proposition: Lemma Exists_eq : forall A (p:A->bool) (P:A->Prop) l, isTrue_pred p P -> Exists p l = isTrue (LibList.Exists P l).
proof: Proof. Proof using. introv E. extens. induction l as [|x l']; simpl; rew_listx in *; rew_bool_eq in *. { iff*. } { rewrite E. rew_bool_eq. iff*. } Qed.
imports: TLC(LibTactics LibReflect)