Faithfully Reflecting the Structure of Informal Mathematical Proofs into Formal Type Theories. - Gueorgui I. Jojgov; Rob Nederpelt; M. Scheffer (MKM Symposium, 2003)