---

Step * of Lemma firstn-le-before

∀[the_es:EO]. ∀[e:E]. ∀[n:ℕ].  firstn(n + 1;≤loc(e)) ~ ≤loc(before(e)[n]) supposing n < ||before(e)||
BY
{ ((UnivCD THENA Auto) THEN (FLemma `firstn-before` [-1] THENA Auto)) }

1
1. the_es : EO
2. e : E
3. n : ℕ
4. n < ||before(e)||
5. firstn(n;before(e)) ~ before(before(e)[n])
⊢ firstn(n + 1;≤loc(e)) ~ ≤loc(before(e)[n])

---

Latex:


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


By

((UnivCD  THENA  Auto)  THEN  (FLemma  `firstn-before`  [-1]  THENA  Auto))

---

Home Index