Commit 2024-06-08 06:05 ef090d9b

fix: remove unused arguments in norm_mkPiAlgebraFin (#13628) As reported on Zulip, norm_mkPiAlgebraFin and norm_mkPiAlgebraFin_le_of_pos contain unused arguments. I fixed it by deleting the offending variables from the variable command, as these weren't used anywhere else. As a result two proofs don't need to specify this unused argument anymore.