---

Step * of Lemma firstn-before

∀[the_es:EO]. ∀[e:E]. ∀[n:ℕ].  firstn(n;before(e)) ~ before(before(e)[n]) supposing n < ||before(e)||
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀the_es:EO. ∀e:E. ∀n:ℕ.  (n < ||before(e)|| ⇒ (firstn(n;before(e)) ~ before(before(e)[n])))

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e:E].  \mforall{}[n:\mBbbN{}].    firstn(n;before(e))  \msim{}  before(before(e)[n])  su\000Cpposing  n  <  ||before(e)||


By

(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index