proposition: Lemma weak_excluded_middle_iff_classical_de_morgan_law : weak_excluded_middle <-> classical_de_morgan_law.
proof: Proof. split; [intro WEM|intro CDML]; intros A *. - destruct (WEM A); tauto. - destruct (CDML A (~A)); tauto. Qed.
imports: PropExtensionalityFacts Hurkens