---

Step * 3 2 of Lemma assert-eq_mFO


1. isall : 𝔹
2. var : ℤ
3. body : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(body;y);body = y ∈ mFOL())
5. i1 : 𝔹
6. ¬i1 = isall
7. v1 : ℤ
8. b1 : mFOL()
9. uiff(↑eq_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body) = b1 ∈ mFOL())
⊢ uiff(↑(inr ⋅ );mFOquant(isall;var;body) = mFOquant(i1;v1;b1) ∈ mFOL())
BY
{ (Fold `bfalse` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  isall  :  \mBbbB{}
2.  var  :  \mBbbZ{}
3.  body  :  mFOL()
4.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(body;y);body  =  y)
5.  i1  :  \mBbbB{}
6.  \mneg{}i1  =  isall
7.  v1  :  \mBbbZ{}
8.  b1  :  mFOL()
9.  uiff(\muparrow{}eq\_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body)  =  b1)
\mvdash{}  uiff(\muparrow{}(inr  \mcdot{}  );mFOquant(isall;var;body)  =  mFOquant(i1;v1;b1))


By

---

Latex:
(Fold  `bfalse`  0  THEN  Auto)

---

Home Index