---

Step * 1 1 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. 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. x:vdf-eq(A;f;firstn(n - 1;L)) ⋂ let tr = L[n - 1] in
                                        (fst(tr)) = (f firstn(n - 1;L) (fst(snd(tr)))) ∈ A
⊢ Ax ∈ x:vdf-eq(A;f;firstn(n - 1;L)) ⋂ let tr = L[n - 1] in
                                           (fst(tr)) = (f firstn(n - 1;L) (fst(snd(tr)))) ∈ A
BY
{ (DepIsectHD (-1)
   THEN DepIsectCD
   THEN ((BackThruSomeHyp THEN Auto) ORELSE (All (RepUR ``let``) THEN MemCD))
   THEN UseWitness ⌜%3⌝⋅
   THEN Auto) }

---

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.  n  :  \mBbbZ{}
7.  0  <  n
8.  ((n  -  1)  \mleq{}  ||L||)  {}\mRightarrow{}  vdf-eq(A;f;firstn(n  -  1;L))  {}\mRightarrow{}  (Ax  \mmember{}  vdf-eq(A;f;firstn(n  -  1;L)))
9.  n  \mleq{}  ||L||
10.  x:vdf-eq(A;f;firstn(n  -  1;L))  \mcap{}  let  tr  =  L[n  -  1]  in
                                                                                (fst(tr))  =  (f  firstn(n  -  1;L)  (fst(snd(tr))))
\mvdash{}  Ax  \mmember{}  x:vdf-eq(A;f;firstn(n  -  1;L))  \mcap{}  let  tr  =  L[n  -  1]  in
                                                                                      (fst(tr))  =  (f  firstn(n  -  1;L)  (fst(snd(tr))))


By

---

Latex:
(DepIsectHD  (-1)
  THEN  DepIsectCD
  THEN  ((BackThruSomeHyp  THEN  Auto)  ORELSE  (All  (RepUR  ``let``)  THEN  MemCD))
  THEN  UseWitness  \mkleeneopen{}\%3\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index