---

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

.....equality..... 
1. fmla : mFOL()@i
2. L : ℤ List@i
⊢ TERMOF{mFOL-bound-rename:o, 1:l, 1:l} ~ TERMOF{mFOL-bound-rename:o, 1:l, i:l}
BY
{ SqequalBySymbComp 900 [] }

---

Latex:


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


By

SqequalBySymbComp  900  []

---

Home Index