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

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

def Lean.Meta.Grind.markNestedSubsingletons (e : Expr) : GrindM Expr

Wrap nested proofs and decidable instances in e with Lean.Grind.nestedProof and Lean.Grind.nestedDecidable-applications. Recall that the congruence closure module has special support for them.

def Lean.Meta.Grind.markProof (e : Expr) : GrindM Expr

Given a proof e, mark it with Lean.Grind.nestedProof