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