proposition: Lemma wp2p1 : forall A:NProp, El A -> El (b2p (p2b A)).
proof: Proof. intros A. unfold p2b. apply or_dep_elim with (b := wem (El A)). + intros nna a. rewrite <- or_elim_redl. cbn. auto. + intros n x. destruct (n x). Qed.
imports: PropExtensionalityFacts Hurkens