lean2/tests/lean/tactic_var_bug.lean.expected.out