---

Step * of Lemma very-dep-fun_wf

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type].  (very-dep-fun(A;B;a,b.C[a;b]) ∈ Type)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].    (very-dep-fun(A;B;a,b.C[a;b])  \mmember{}  Type)


By

---

Latex:
ProveWfLemma

---

Home Index