A Two-Level Approach Towards Lean Proof-Checking. - Gilles Barthe; Mark Ruys; Henk Barendregt (TYPES, 1995)