import Algebra.Monad

  proofLeftIdentity (x::xs) = rewrite proofLeftIdentity xs in Refl

  proofLeftIdentity (x::xs) = rewrite Monoid.proofLeftIdentity xs in Refl

  proofRightIdentity (y::ys) = rewrite proofRightIdentity ys in Refl

  proofRightIdentity (y::ys) = rewrite Monoid.proofRightIdentity ys in Refl

partial

public export
Monad LinkedList where
  bind Nil _ = Nil
  bind (x::xs) f = f x <> (xs `bind` f)
  proofLeftIdentity x f = rewrite concatNil (f x) in Refl
  proofRightIdentity Nil = Refl
  proofRightIdentity (x::xs) with (Monad.proofRightIdentity xs)
    proofRightIdentity (_::_) | prf = rewrite prf in Refl
  proofAssociativity Nil f g = Refl
  proofAssociativity (x::xs) f g with (f x)
    proofAssociativity (x::xs) f g | Nil = rewrite proofAssociativity xs f g in Refl
    proofAssociativity (x::xs) f g | (r::rs) = ?holeAssociativity