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

Adds e to congruence table.

def Lean.Meta.Grind.isMorallyIff (e : Expr) : Bool

Returns true if e is of the form @Eq Prop a b

def Lean.Meta.Grind.activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit