---

Step * of Lemma vdf-eq-subtype

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) ⊆r (∀[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 Intros
   THEN (D 0 THENA (InstHyp [⌜f⌝;⌜L⌝] (-4)⋅ THEN Auto))
   THEN InstHyp [⌜f⌝;⌜L⌝] (-5)⋅
   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)  \msubseteq{}r  (\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  Intros
  THEN  (D  0  THENA  (InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto))
  THEN  InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  (-5)\mcdot{}
  THEN  Auto)

---

Home Index