LeanPool.FormalizationOfBoundedArithmetic.MathlibSimps

def commandMkDelta0FromModelTheory : Lean.ParserDescr

Add existing Mathlib model-theory simp lemmas to the local delta0_simps simp set.

Equations

• commandMkDelta0FromModelTheory = Lean.ParserDescr.node `commandMkDelta0FromModelTheory 1024 (Lean.ParserDescr.symbol "mkDelta0FromModelTheory")