---

Step * of Lemma mFO-equal_wf

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

---

Latex:


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


By

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

---

Home Index