---

Step * of Lemma cbva_seq_wf

∀[T,U:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[F:(funtype(m;A;T) ⟶ T) ⟶ U].
  (cbva_seq(L; F; m) ∈ U)
BY
{ (ProveWfLemma THEN RepUR ``funtype`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,U:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[A:\mBbbN{}m  {}\mrightarrow{}  ValueAllType].  \mforall{}[L:i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;A;A  i)].
\mforall{}[F:(funtype(m;A;T)  {}\mrightarrow{}  T)  {}\mrightarrow{}  U].
    (cbva\_seq(L;  F;  m)  \mmember{}  U)


By

---

Latex:
(ProveWfLemma  THEN  RepUR  ``funtype``  0  THEN  Auto)

---

Home Index