Support for type class LawfulEqCmp.

def Lean.Meta.Grind.getLawfulEqCmpThm? (op : Expr) : GrindM (Option Expr)

If op implements LawfulEqCmp, then returns the proof term for ∀ a b, op a b = .eq → a = b

def Lean.Meta.Grind.getLawfulEqCmpThm?.go? (op : Expr) : MetaM (Option Expr)

def Lean.Meta.Grind.propagateLawfulEqCmp (e : Expr) : GoalM Unit