proposition: Theorem paradox : forall B:Prop, B.
proof: Proof. intros B. unshelve (refine (mparadox (exist _ bool (fun x => x)) _ _ _ _ (exist _ B (fun x => x)))). + intros p. red. red. exact (p2b (El p)). + cbn. intros b. red. exists (b2p b). exact (fun x => x). + cbn. intros [A H]. cbn. apply p2p1. + cbn. intros [A H]. cbn. apply p2p2. Qed.