---

Step * of Lemma vdf-eq-witness

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].
  Ax ∈ vdf-eq(A;f;L) supposing vdf-eq(A;f;L)
BY
{ 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. vdf-eq(A;f;L)
⊢ Ax ∈ vdf-eq(A;f;L)

---

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].
    Ax  \mmember{}  vdf-eq(A;f;L)  supposing  vdf-eq(A;f;L)


By

---

Latex:
Auto

---

Home Index