---

Step * 2 1 of Lemma nth_tl_append


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
BY
{ ((RecUnfold `nth_tl` 0 THEN SplitOnConclITE THEN Reduce 0) THEN Try (Complete (Auto'))) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RecUnfold  `nth\_tl`  0  THEN  SplitOnConclITE  THEN  Reduce  0)  THEN  Try  (Complete  (Auto')))

---

Home Index