proposition: Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett.
proof: Proof. intros EM A B. destruct (EM B) as [HB|HnotB]. - left; intros _; exact HB. - right; intros HB; destruct (HnotB HB). Qed.
imports: PropExtensionalityFacts Hurkens