proposition: Lemma or_def : or = (fun p : Prop => fun q : Prop => forall r : Prop, (p -> r) -> (q -> r) -> r).
proof: Proof. apply fun_ext; intro p; apply fun_ext; intro q. apply prop_ext. intros pq r pr qr. destruct pq. apply (pr H). apply (qr H). intro h. apply h. intro hp. left. exact hp. intro hq. right. exact hq. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts