---

Step * of Lemma vdf-eq-implies2

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].
  (vdf-eq(A;f;L) ⇒ {∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A)})
BY
{ (InstLemma `vdf-eq-implies` []⋅
   THEN RepeatFor 3 (ParallelLast')
   THEN Intros
   THEN InstHyp [⌜||L||⌝;⌜f⌝;⌜L⌝] 4⋅
   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].
    (vdf-eq(A;f;L)  {}\mRightarrow{}  \{\mforall{}[i:\mBbbN{}||L||].  ((fst(L[i]))  =  (f  firstn(i;L)  (fst(snd(L[i])))))\})


By

---

Latex:
(InstLemma  `vdf-eq-implies`  []\mcdot{}
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Intros
  THEN  InstHyp  [\mkleeneopen{}||L||\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)

---

Home Index