TRE: a Coq implementation of Tarjan & Kaplan "Real-Time Deques with Catenation"