proposition: Lemma wp2p2 : b1 <> b2 -> forall A:NProp, El (b2p (p2b A)) -> El A.
proof: Proof. intro not_eq_b1_b2. intros A. unfold p2b. apply or_dep_elim with (b := wem (El A)). + cbn. intros x _. destruct A. cbn in x |- *. auto. + intros na. rewrite <- or_elim_redr. cbn. intros h. destruct (h not_eq_b1_b2). Qed.
imports: PropExtensionalityFacts Hurkens