proposition: Lemma set_Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) X : {set_Forall P X} + {set_Exists Q X}.
proof: Proof. refine (cast_if (Forall_Exists_dec P Q dec (elements X))); [by apply set_Forall_elements|by apply set_Exists_elements]. Defined.
imports: stdpp(relations) stdpp(options)