---

Step * of Lemma ma-valtype-subtype

∀[k:Knd]. ∀[da,da':a:Knd fp-> Type].  Valtype(da';k) ⊆r Valtype(da;k) supposing da ⊆ da'
BY
{ (Auto THEN Unfold `ma-valtype` 0 THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  \mforall{}[da,da':a:Knd  fp->  Type].    Valtype(da';k)  \msubseteq{}r  Valtype(da;k)  supposing  da  \msubseteq{}  da'


By

(Auto  THEN  Unfold  `ma-valtype`  0  THEN  Auto)

---

Home Index