---

Step * of Lemma CV_wf

∀[A:Type]. ∀[F:t:ℕ ⟶ (ℕt ⟶ A) ⟶ A].  (CV(F) ∈ ℕ ⟶ A)
BY
{ (Auto THEN Assert ⌜∀t:ℕ. (CV(F) ∈ ℕt ⟶ A)⌝⋅) }

1
.....assertion..... 
1. A : Type
2. F : t:ℕ ⟶ (ℕt ⟶ A) ⟶ A
⊢ ∀t:ℕ. (CV(F) ∈ ℕt ⟶ A)

2
1. A : Type
2. F : t:ℕ ⟶ (ℕt ⟶ A) ⟶ A
3. ∀t:ℕ. (CV(F) ∈ ℕt ⟶ A)
⊢ CV(F) ∈ ℕ ⟶ A

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[F:t:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}t  {}\mrightarrow{}  A)  {}\mrightarrow{}  A].    (CV(F)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  A)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}t:\mBbbN{}.  (CV(F)  \mmember{}  \mBbbN{}t  {}\mrightarrow{}  A)\mkleeneclose{}\mcdot{})

---

Home Index