module Data.Bool.Extra %default total public exportandSameNeutral : (x : Bool) -> x && x = xandSameNeutral False = ReflandSameNeutral True = Refl public exportandFalseFalse : (x : Bool) -> x && False = FalseandFalseFalse False = ReflandFalseFalse True = Refl public exportandTrueNeutral : (x : Bool) -> x && True = xandTrueNeutral False = ReflandTrueNeutral True = Refl public exportorSameNeutral : (x : Bool) -> x || x = xorSameNeutral False = ReflorSameNeutral True = Refl public exportorFalseNeutral : (x : Bool) -> x || False = xorFalseNeutral False = ReflorFalseNeutral True = Refl public exportorTrueTrue : (x : Bool) -> x || True = TrueorTrueTrue False = ReflorTrueTrue True = Refl public exportorSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = xorSameAndRightNeutral False _ = ReflorSameAndRightNeutral True _ = Refl