Support for type class ReflCmp.

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

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

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

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