@mcc also if you want boolean equality on lists (==) should just work without importing anything because it's provided by the Eq typeclass https://idris2docs.sinyax.net/data/prelude/docs/Prelude.Types.src.html#line391 so if a has an Eq typeclass then so does List a automatically