proposition: Lemma is_False P : (P = False) = ~ P.
proof: Proof. apply prop_ext; intro h. rewrite h. intro i. exact i. apply prop_ext; intro i. apply h. apply i. apply False_rec. exact i. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts