---

Step * 1 of Lemma reject_eq_firstn_nth_tl


1. T : Type
2. u : T
3. v : T List
4. ∀i:ℕ||v||. (v\[i] ~ firstn(i;v) @ nth_tl(1 + i;v))
5. i : ℤ
6. 0 ≤ i < ||v|| + 1
7. i = 0 ∈ ℤ
⊢ [u / v]\[i] ~ firstn(i;[u / v]) @ nth_tl(1 + i;[u / v])
BY
{ ((HypSubst' (-1) 0 THENA Auto)
   THEN ThinVar `i'
   THEN (RWO "first0" 0 THENA Auto)
   THEN Reduce 0
   THEN RWO "reject_cons_hd_sq" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}i:\mBbbN{}||v||.  (v\mbackslash{}[i]  \msim{}  firstn(i;v)  @  nth\_tl(1  +  i;v))
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i  <  ||v||  +  1
7.  i  =  0
\mvdash{}  [u  /  v]\mbackslash{}[i]  \msim{}  firstn(i;[u  /  v])  @  nth\_tl(1  +  i;[u  /  v])


By

---

Latex:
((HypSubst'  (-1)  0  THENA  Auto)
  THEN  ThinVar  `i'
  THEN  (RWO  "first0"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWO  "reject\_cons\_hd\_sq"  0
  THEN  Auto)

---

Home Index