---

Step * of Lemma vdf-eq-firstn-implies

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[L:(a:A × b:B × C[a;b]) List]. ∀[j:ℕ||L||].
  (vdf-eq(A;f;firstn(j;L)) ⇒ {∀[i:ℕj]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)})
BY
{ (InstLemma `vdf-eq-implies2` []⋅
   THEN RepeatFor 4 (ParallelLast')
   THEN Unfold `guard` 0
   THEN Intros
   THEN (InstHyp [⌜firstn(j;L)⌝] 5⋅ THENA Auto)
   THEN (D -1 With ⌜i⌝  THENA Auto)
   THEN RWO "select-firstn firstn-firstn" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[f:very-dep-fun(A;B;a,b.C[a;b])].  \mforall{}[L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List].
\mforall{}[j:\mBbbN{}||L||].
    (vdf-eq(A;f;firstn(j;L))  {}\mRightarrow{}  \{\mforall{}[i:\mBbbN{}j].  ((fst(L[i]))  =  (f  firstn(i;L)  (fst(snd(L[i])))))\})


By

---

Latex:
(InstLemma  `vdf-eq-implies2`  []\mcdot{}
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Unfold  `guard`  0
  THEN  Intros
  THEN  (InstHyp  [\mkleeneopen{}firstn(j;L)\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RWO  "select-firstn  firstn-firstn"  (-1)
  THEN  Auto)

---

Home Index