A. Lolic, A. Leitsch: "Extraction of Expansion Trees"; Journal of Automated Reasoning, 62 (2019), 3; 393 - 430.
https://publik.tuwien.ac.at/files/publik_287158.pdf