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