---

Step * of Lemma vdf-eq_wf

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type].  ∀L:(a:A × b:B × C[a;b]) List. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. (vdf-eq(A;f;L) ∈ ℙ)
BY
{ (InstLemma `vdf-wf` [] THEN RepeatFor 3 (ParallelLast') THEN Intros THEN Unhide) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. ∀n:ℕ
     ((vdf(A;B;a,b.C[a;b];n) ∈ Type)
     ∧ (∀f:vdf(A;B;a,b.C[a;b];n). ∀L:(a:A × b:B × C[a;b]) List.  ((||L|| ≤ (n + 1)) ⇒ (vdf-eq(A;f;L) ∈ ℙ))))
5. L : (a:A × b:B × C[a;b]) List
6. f : very-dep-fun(A;B;a,b.C[a;b])
⊢ vdf-eq(A;f;L) ∈ ℙ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].
    \mforall{}L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List.  \mforall{}[f:very-dep-fun(A;B;a,b.C[a;b])].  (vdf-eq(A;f;L)  \mmember{}  \mBbbP{})


By

---

Latex:
(InstLemma  `vdf-wf`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Intros  THEN  Unhide)

---

Home Index