fix: use the matched lambdas in `grind` constant-function propagation

This PR fixes a kernel error in `grind` when it combines equations between constant functions and an equivalence class contains more than one lambda.

`propagateUnitConstFuns` built the equality proof between the first lambda of each equivalence class instead of the lambdas `lam₁` and `lam₂` whose bodies form the asserted fact. It now uses `mkEqProof lam₁ lam₂`.

Closes #15721

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>