lean2/tests/lean/interactive/proof_qed.input