lean2/tests/lean/print_ax1.lean