∀(a : Type) → ../../../../../Prelude/Monoid (List { index : Natural, value : a })