Type-safe verified Red-Black Trees in Idris 2