I would like to do Canonical stuff := ... but within a proof.
Canonical stuff := ...
Last updated: Mar 28 2024 at 11:01 UTC