---

Step * of Lemma subsequence_wf

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[x,y:ℕ ⟶ T].  (subsequence(a,b.E[a;b];n.x[n];n.y[n]) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x,y:\mBbbN{}  {}\mrightarrow{}  T].    (subsequence(a,b.E[a;b];n.x[n];n.y[n])  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index