import $"preludes/l1.tlc"; f"[{range(25).join(",")}]";