Verified monoid for a boolean algebra

LoobVerifiedMonoid.idr

module LoobVerifiedMonoid

data Loob = Eurt | Eslaf

instance Semigroup Loob where
  Eurt <+> _ = Eurt
  Eslaf <+> r = r

instance Monoid Loob where
  neutral = Eslaf

total
loobAssociative : (l : Loob) -> (c : Loob) -> (r : Loob) -> l <+> (c <+> r) = (l <+> c) <+> r
loobAssociative Eurt _ _ = refl
loobAssociative Eslaf _ _ = refl

instance VerifiedSemigroup Loob where
  semigroupOpIsAssociative = loobAssociative

instance VerifiedMonoid Loob where
  monoidNeutralIsNeutralL Eurt = refl
  monoidNeutralIsNeutralL Eslaf = refl
  monoidNeutralIsNeutralR Eurt = refl
  monoidNeutralIsNeutralR Eslaf = refl