proposition: Lemma Godel_Dummett_weak_excluded_middle : GodelDummett -> weak_excluded_middle.
proof: Proof. intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA]. - left; intro HnotA; apply (HnotA (HnotAA HnotA)). - right; intro HA; apply (HAnotA HA HA). Qed.
imports: PropExtensionalityFacts Hurkens