make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn
Attach a file by drag & drop or click to upload
Ralf Jung authored