law and_not_self

bend-mathlib@0.8.1.0 · bool.bend:219

import Base

219# A boolean and its negation are never both true: a and (not a) is false.
220law and_not_self:
221  for a: Bool
222  {Bool.and(a, Bool.not(a)) == False{} : Bool}