@[reducible, inline]
Equations
Instances For
Equations
- LO.«term𝗧𝗔» = Lean.ParserDescr.node `LO.«term𝗧𝗔» 1024 (Lean.ParserDescr.symbol "𝗧𝗔")
Instances For
instance
LO.FirstOrderTrueArith.instWeakerThanSentenceORingTheoryOfModelsTheoryNat
(T : FirstOrder.Theory ℒₒᵣ)
[ℕ ⊧ₘ* T]
: