---

Step * of Lemma dl-same-sem_wf

∀[x:dl-Obj()]. ∀[K:Type]. ∀[r,s:if dl-kind(x) =a "prog" then K ⟶ K ⟶ ℙ else K ⟶ ℙ fi ].  (dl-same-sem(x;K;r;s) ∈ ℙ)
BY
{ (ProveWfLemma THEN Eliminate ⌜dl-kind(x)⌝⋅ THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:dl-Obj()].  \mforall{}[K:Type].  \mforall{}[r,s:if  dl-kind(x)  =a  "prog"  then  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}  else  K  {}\mrightarrow{}  \mBbbP{}  fi  ].
    (dl-same-sem(x;K;r;s)  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  Eliminate  \mkleeneopen{}dl-kind(x)\mkleeneclose{}\mcdot{}  THEN  All  Reduce  THEN  Auto)

---

Home Index