---

Step * 2 of Lemma nth_tl_append


1. T : Type
2. u : T
3. v : T List
4. ∀[bs:T List]. (nth_tl(||v||;v @ bs) ~ bs)
⊢ ∀[bs:T List]. (nth_tl(||v|| + 1;[u / (v @ bs)]) ~ bs)
BY
{ ParallelLast }

1
1. T : Type
2. u : T
3. v : T List
4. [bs] : T List
5. nth_tl(||v||;v @ bs) ~ bs
⊢ nth_tl(||v|| + 1;[u / (v @ bs)]) ~ bs

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[bs:T  List].  (nth\_tl(||v||;v  @  bs)  \msim{}  bs)
\mvdash{}  \mforall{}[bs:T  List].  (nth\_tl(||v||  +  1;[u  /  (v  @  bs)])  \msim{}  bs)


By

---

Latex:
ParallelLast

---

Home Index