proposition: Theorem paradox : forall B:NProp, El B.
proof: Proof. intros B. unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + exact bool. + exact p2b. + exact b2p. + exact B. + exact h. + cbn. auto. + cbn. auto. + cbn. auto. Qed.