---

Step * 2 of Lemma vdf-eq-firstn


1. A : Type
2. f : Top
3. L : (a:Top × b:Top × Top) List
4. i : ℕ||L||
5. ¬i + 1 < 1
6. @0 : Base
⊢ let a,b,c = firstn(i + 1;L)[i] in 
a = (f firstn(i;firstn(i + 1;L)) b) ∈ A ~ (fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A
BY
{ ((RWO "select-firstn firstn-firstn" 0 THENA Auto)
   THEN (GenConclTerm ⌜L[i]⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  Top
3.  L  :  (a:Top  \mtimes{}  b:Top  \mtimes{}  Top)  List
4.  i  :  \mBbbN{}||L||
5.  \mneg{}i  +  1  <  1
6.  @0  :  Base
\mvdash{}  let  a,b,c  =  firstn(i  +  1;L)[i]  in 
a  =  (f  firstn(i;firstn(i  +  1;L))  b)  \msim{}  (fst(L[i]))  =  (f  firstn(i;L)  (fst(snd(L[i]))))


By

---

Latex:
((RWO  "select-firstn  firstn-firstn"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}L[i]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index