def Lean.Meta.Grind.isDiseq (a b : Expr) : GoalM Bool

Returns true if a and b are known to be disequal. See getDiseqFor?

def Lean.Meta.Grind.mkDiseqProof? (a b : Expr) : GoalM (Option Expr)

Returns a proof for true if a and b are known to be disequal. See getDiseqFor?

def Lean.Meta.Grind.mkDiseqProof (a b : Expr) : GoalM Expr