---

Step * 1 of Lemma vdf-eq-witness


1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. L : (a:A × b:B × C[a;b]) List
6. vdf-eq(A;f;L)
⊢ Ax ∈ vdf-eq(A;f;L)
BY
{ ((Enough to prove ∀n:ℕ. ((n ≤ ||L||) ⇒ vdf-eq(A;f;firstn(n;L)) ⇒ (Ax ∈ vdf-eq(A;f;firstn(n;L))))
     Because (InstHyp [⌜||L||⌝] (-1)⋅ THEN Auto))
   THEN Thin (-1)
   THEN InductionOnNat
   THEN Auto
   THEN Try (((RWO "first0" 0 THENA Auto) THEN RepUR ``vdf-eq dep-all`` 0 THEN Auto))) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. L : (a:A × b:B × C[a;b]) List
6. n : ℤ
7. 0 < n
8. ((n - 1) ≤ ||L||) ⇒ vdf-eq(A;f;firstn(n - 1;L)) ⇒ (Ax ∈ vdf-eq(A;f;firstn(n - 1;L)))
9. n ≤ ||L||
10. vdf-eq(A;f;firstn(n;L))
⊢ Ax ∈ vdf-eq(A;f;firstn(n;L))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type
4.  f  :  very-dep-fun(A;B;a,b.C[a;b])
5.  L  :  (a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List
6.  vdf-eq(A;f;L)
\mvdash{}  Ax  \mmember{}  vdf-eq(A;f;L)


By

---

Latex:
((Enough  to  prove  \mforall{}n:\mBbbN{}.  ((n  \mleq{}  ||L||)  {}\mRightarrow{}  vdf-eq(A;f;firstn(n;L))  {}\mRightarrow{}  (Ax  \mmember{}  vdf-eq(A;f;firstn(n;L))))
      Because  (InstHyp  [\mkleeneopen{}||L||\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  Thin  (-1)
  THEN  InductionOnNat
  THEN  Auto
  THEN  Try  (((RWO  "first0"  0  THENA  Auto)  THEN  RepUR  ``vdf-eq  dep-all``  0  THEN  Auto)))

---

Home Index