Verified Purely Functional Catenable Real-Time Deques