A basic "equality resolution" procedure.

def Lean.Meta.Grind.eqResolution (prop : Expr) : MetaM (Option (Expr × Expr))

A basic "equality resolution" procedure: Given a proposition prop with a proof proof, it attempts to resolve equality hypotheses using isDefEq. For example, it reduces ∀ x y, f x = f (g y y) → g x y = y to ∀ y, g (g y y) y = y, and ∀ (x : Nat), f x ≠ f a to False. If successful, the result is a pair (prop', proof), where prop' is the simplified proposition, and proof : prop → prop'

Equations

• One or more equations did not get rendered due to their size.