Skip to content

add bool_decide_negb

Ralf Jung requested to merge ralf/bool_decide_negb into master

I had to move up all the Decision stuff since the new lemma needs the not_dec instance.

Proof by Yun-Sheng.

Merge request reports