Commit 2022-11-10 15:12 d61f638a

chore(data/finsupp/defs): redefine finsupp.single as pi.single (#17356) This also brings it in line with dfinsupp.single. Note that the two are still not defeq due to different decidability instances, but things are least more consistent now. In order to make some proofs still unify, this makes some type arguments explicit to constant_coeff_C and constant_coeff_X. These lemmas should have had these as explicit arguments anyway, as the type can't be inferred from the other arguments.