---

Step * of Lemma dl-prog-sem_wf

∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P:ℕ ⟶ K ⟶ ℙ]. ∀[alpha:Prog].  ([|alpha|] ∈ K ⟶ K ⟶ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[K:Type].  \mforall{}[R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[alpha:Prog].    ([|alpha|]  \mmember{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index