proposition: Lemma ex_iff: forall {A: Type} P Q, (forall x: A, P x <-> Q x) -> (ex P <-> ex Q).
proof: Proof. intros. split; intros [x ?]; exists x; firstorder. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Program.Basics