These refer to the misformalizations identified and fixed in Lean as part of #322.
These refer to the misformalizations identified and fixed in Lean as part of #322.