---

Step * 2 of Lemma firstn_append


1. u : Top
2. v : Top List
3. ∀[L2:Top List]. ∀[n:ℕ||v|| + 1].  (firstn(n;v @ L2) ~ firstn(n;v))
⊢ ∀[L2:Top List]. ∀[n:ℕ(||v|| + 1) + 1].
    (if 0 <z n then [u / firstn(n - 1;v @ L2)] else [] fi  ~ if 0 <z n then [u / firstn(n - 1;v)] else [] fi )
BY
{ ((((UnivCD THENA Auto) THEN SplitOnConclITE) THENA Auto) THEN EqCD THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. ∀[L2:Top List]. ∀[n:ℕ||v|| + 1].  (firstn(n;v @ L2) ~ firstn(n;v))
4. L2 : Top List
5. n : ℕ(||v|| + 1) + 1
6. 0 < n
⊢ firstn(n - 1;v @ L2) ~ firstn(n - 1;v)

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[L2:Top  List].  \mforall{}[n:\mBbbN{}||v||  +  1].    (firstn(n;v  @  L2)  \msim{}  firstn(n;v))
\mvdash{}  \mforall{}[L2:Top  List].  \mforall{}[n:\mBbbN{}(||v||  +  1)  +  1].
        (if  0  <z  n  then  [u  /  firstn(n  -  1;v  @  L2)]  else  []  fi    \msim{}  if  0  <z  n
        then  [u  /  firstn(n  -  1;v)]
        else  []
        fi  )


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  SplitOnConclITE)  THENA  Auto)  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index