---

Step * 1 of Lemma FOL-rename-bound-to-avoid_wf

.....equality..... 
1. fmla : mFOL()
2. L : ℤ List
⊢ TERMOF{FOL-bound-rename:o, 1:l, 1:l} ~ TERMOF{FOL-bound-rename:o, 1:l, i:l}
BY
{ SqequalBySymbComp200 }

---

Latex:

---

Latex:
.....equality..... 
1.  fmla  :  mFOL()
2.  L  :  \mBbbZ{}  List
\mvdash{}  TERMOF\{FOL-bound-rename:o,  1:l,  1:l\}  \msim{}  TERMOF\{FOL-bound-rename:o,  1:l,  i:l\}


By

---

Latex:
SqequalBySymbComp200

---

Home Index