Overheard: “equality of proofs via beta reduction”.