Re: [cbc] Problems with automatic proving in Rodin