---

Step * 1 1 of Lemma firstn_firstn

.....truecase..... 
1. u : Top
2. v : Top List
3. ∀[n:ℤ]. ∀[m:ℕn + 1].  (firstn(m;firstn(n;v)) ~ firstn(m;v))
4. n : ℤ
5. m : ℕn + 1
6. 0 < n
7. 0 < m
⊢ [u / firstn(m - 1;firstn(n - 1;v))] ~ [u / firstn(m - 1;v)]
BY
{ (EqCD THEN Try (Trivial) THEN Try ((BackThruSomeHyp THEN Auto')) THEN Auto')⋅ }

---

Latex:

---

Latex:
.....truecase..... 
1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[n:\mBbbZ{}].  \mforall{}[m:\mBbbN{}n  +  1].    (firstn(m;firstn(n;v))  \msim{}  firstn(m;v))
4.  n  :  \mBbbZ{}
5.  m  :  \mBbbN{}n  +  1
6.  0  <  n
7.  0  <  m
\mvdash{}  [u  /  firstn(m  -  1;firstn(n  -  1;v))]  \msim{}  [u  /  firstn(m  -  1;v)]


By

---

Latex:
(EqCD  THEN  Try  (Trivial)  THEN  Try  ((BackThruSomeHyp  THEN  Auto'))  THEN  Auto')\mcdot{}

---

Home Index