---

Step * of Lemma dl-sem_wf

∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P:ℕ ⟶ K ⟶ ℙ].
  (dl-sem(K;n.R[n];m.P[m]) ∈ d:dl-Obj() ⟶ if dl-kind(d) =a "prog" then K ⟶ K ⟶ ℙ else K ⟶ ℙ fi )
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[K:Type].  \mforall{}[R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].
    (dl-sem(K;n.R[n];m.P[m])  \mmember{}  d:dl-Obj()  {}\mrightarrow{}  if  dl-kind(d)  =a  "prog"  then  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}  else  K  {}\mrightarrow{}  \mBbbP{}  fi  )


By

---

Latex:
ProveWfLemma

---

Home Index