---

Step * of Lemma mFO-equal_wf

∀[x:mFOL()]. (mFO-equal(x) ∈ mFOL() ⟶ 𝔹)
BY
{ xxx(Unfold `bool` 0 THEN ProveWfLemma THEN All (Fold `bool`)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[x:mFOL()].  (mFO-equal(x)  \mmember{}  mFOL()  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
xxx(Unfold  `bool`  0  THEN  ProveWfLemma  THEN  All  (Fold  `bool`)\mcdot{}  THEN  Auto)xxx

---

Home Index