make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn
Ralf Jung authored