def Aesop.BuiltinRules.destructProductsCore (goal : Lean.MVarId) (md : Lean.Meta.TransparencyMode) : BaseM (Lean.MVarId × Array Script.LazyStep)

partial def Aesop.BuiltinRules.destructProductsCore.go (md : Lean.Meta.TransparencyMode) (i : Nat) (goal : Lean.MVarId) : ScriptM Lean.MVarId

def Aesop.BuiltinRules.destructProducts : RuleTac