proposition: Theorem not_ex_all_not_proof : forall A (B : A -> Prop), ~(exists x, B x) -> forall x, ~B x.
proof: Proof. intros A B H x Hx. elim H. now exists x. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping