Proving Tree Algorithms for Succinct Data Structures. - Reynald Affeldt; Jacques Garrigue; Xuanrui Qi; Kazunari Tanaka (ITP, 2019)