proposition: Lemma Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) : ∀ l, {Forall P l} + {Exists Q l}.
proof: Proof. refine ( fix go l := match l return {Forall P l} + {Exists Q l} with | [] => left _ | x :: l => cast_if_and (dec x) (go l) end); clear go; intuition. Defined.
imports: stdpp(options)