fact: Definition not (e : bexpr) := match e with | Bval true => Bval false | Bval false => Bval true | _ => Bnot e end.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String