proposition: Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
proof: Proof. unfold p2b; intro A; apply or_dep_elim with (b := em A); unfold b2p; intros. - apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). - destruct (b H). Qed.
imports: PropExtensionalityFacts Hurkens