---

Step * of Lemma locknd_wf

∀[i:Id]. ∀[k:Knd].  (locknd(i;k) ∈ LocKnd)
BY
{ (Auto
   THEN Unfold `locknd` 0
   THEN MemTypeCD
   THEN Auto
   THEN KindCases
   THEN BLemma `assert-hasloc` 
   THEN Auto
   THEN (All Reduce THEN Auto)⋅) }

---

Latex:


\mforall{}[i:Id].  \mforall{}[k:Knd].    (locknd(i;k)  \mmember{}  LocKnd)


By

(Auto
  THEN  Unfold  `locknd`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  KindCases
  THEN  BLemma  `assert-hasloc` 
  THEN  Auto
  THEN  (All  Reduce  THEN  Auto)\mcdot{})

---

Home Index