Commit 2023-03-16 03:28 2e9801b6
View on Github →feat: let apply_fun use CoeFun and dependent functions (#2890)
Changes apply_fun to use the main function application elaborator, then uses Lean.MVarId.congrN to solve for a congruence proof. This means that apply_fun f at h should work whenever f applies to both sides of the equation h (even when coercions need to be involved).