---

Step * of Lemma vdf-eq-implies

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[n:ℕ]. ∀[f:vdf(A;B;a,b.C[a;b];n)]. ∀[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)) supposing ||L|| ≤ (n + 1)
BY
{ (InstLemma `vdf-wf+` []
   THEN RepeatFor 4 (ParallelLast')
   THEN D -1
   THEN RepeatFor 3 (Intro)
   THEN (Assert vdf-eq(A;f;L) ∈ ℙ BY
               (Unhide THEN InstHyp [⌜f⌝;⌜L⌝] 6⋅ THEN Auto))
   THEN Intro
   THEN RenameVar `x' (-1)
   THEN UseWitness ⌜x⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[f:vdf(A;B;a,b.C[a;b];n)].
\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])))))) 
    supposing  ||L||  \mleq{}  (n  +  1)


By

---

Latex:
(InstLemma  `vdf-wf+`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  D  -1
  THEN  RepeatFor  3  (Intro)
  THEN  (Assert  vdf-eq(A;f;L)  \mmember{}  \mBbbP{}  BY
                          (Unhide  THEN  InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  6\mcdot{}  THEN  Auto))
  THEN  Intro
  THEN  RenameVar  `x'  (-1)
  THEN  UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index