module Data.Bool;
  inductive Bool {
    true : Bool;
    false : Bool;
  };

  not : Bool → Bool;
  not true ≔ false;
  not false ≔ true;

  infixr 2 ||;
  || : Bool → Bool → Bool;
  || false a ≔ a;
  || true _ ≔ true;

  infixr 2 &&;
  && : Bool → Bool → Bool;
  && false _ ≔ false;
  && true a ≔ a;

end;