Certified binary search tree on W-types. - Gustavo Arengas (CoRR, 2024)