---

Step * 2 2 of Lemma assert-eq_mFO


1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(left;y);left = y ∈ mFOL())
5. ∀y:mFOL(). uiff(↑eq_mFO(right;y);right = y ∈ mFOL())
6. k1 : Atom
7. k1 ≠ knd ∈ Atom 
8. l1 : mFOL()
9. r1 : mFOL()
10. uiff(↑eq_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right) = l1 ∈ mFOL())
11. uiff(↑eq_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right) = r1 ∈ mFOL())
⊢ uiff(↑(inr ⋅ );mFOconnect(knd;left;right) = mFOconnect(k1;l1;r1) ∈ mFOL())
BY
{ (Fold `bfalse` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  knd  :  Atom
2.  left  :  mFOL()
3.  right  :  mFOL()
4.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(left;y);left  =  y)
5.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(right;y);right  =  y)
6.  k1  :  Atom
7.  k1  \mneq{}  knd  \mmember{}  Atom 
8.  l1  :  mFOL()
9.  r1  :  mFOL()
10.  uiff(\muparrow{}eq\_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right)  =  l1)
11.  uiff(\muparrow{}eq\_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right)  =  r1)
\mvdash{}  uiff(\muparrow{}(inr  \mcdot{}  );mFOconnect(knd;left;right)  =  mFOconnect(k1;l1;r1))


By

---

Latex:
(Fold  `bfalse`  0  THEN  Auto)

---

Home Index