Proof-term reconstruction from TSTP to Agda (2015)