lean2/tests/lean/quot_bug.lean.expected.out