Commit 2025-11-14 17:31 ebbb9b3e

perf(reassoc, to_app, elementwise): don't pass the same proof to the kernel again (#30650) In reassoc, to_app, elementwise, the proof of the original lemma was being used to prove the modified lemma. This is silly, because the modified lemma can be proved using the original lemma directly. Hence, this PR modifies addRelatedDecl to include this optimization. Previously, addRelatedDecl would pass around both the type and the value of the original declaration. This was necessary, because the inferred type of the value might not be identical to the type it is given. Now this is not necessary anymore, because the type of the constant is exactly the type that it is given, so the type can always be obtained with inferType.