proposition: Lemma P_neq_not_P: forall (P:Prop), P <> ~P.
proof: Proof. unfold not; intros. assert (~P). { unfold not; intro. assert (P->False). { rewrite <- H. assumption. } tauto. } assert P. { rewrite H. assumption. } contradiction. Qed.
imports: Coq(ClassicalChoice) Coq(ProofIrrelevance) Coq(FunctionalExtensionality) Coq(Description) ZornsLemma(FunctionPropertiesEns) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(CSB) ZornsLemma(EnsemblesSpec) ZornsLemma(ZornsLemma) ZornsLemma(EnsemblesImplicit) ZornsLemma(CountableTypes) ZornsLemma(FiniteTypes) ZornsLemma(InfiniteTypes) Coq(RelationClasses)