---

Step * of Lemma dl-prop-sem_wf

∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P:ℕ ⟶ K ⟶ ℙ]. ∀[phi:Prop].  ([|phi|] ∈ 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{}[phi:Prop].    ([|phi|]  \mmember{}  K  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index