proposition: Lemma foo2 : (exists x, A -> P x) -> (forall x, ~P x) -> ~A.
proof: Proof. case=> x hx hP hA. apply: (hP x). exact: hx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)