---

Step * of Lemma locknd-spread_wf2

∀[T:Type]. ∀[P:i:Id ─→ k:{k:Knd| ↑hasloc(k;i)}  ─→ T]. ∀[ik:LocKnd].  (let i,k:LocKnd = ik in P[i;k] ∈ T)
BY
{ (Unfolds ``LocKnd locknd-spread`` 0
   THEN Auto
   THEN D 3
   THEN MemTypeCD
   THEN Auto
   THEN HypSubst' 7 4
   THEN Auto
   THEN Reduce (-1)
   THEN Trivial) }

---

Latex:


\mforall{}[T:Type].  \mforall{}[P:i:Id  {}\mrightarrow{}  k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    {}\mrightarrow{}  T].  \mforall{}[ik:LocKnd].
    (let  i,k:LocKnd  =  ik  in  P[i;k]  \mmember{}  T)


By

(Unfolds  ``LocKnd  locknd-spread``  0
  THEN  Auto
  THEN  D  3
  THEN  MemTypeCD
  THEN  Auto
  THEN  HypSubst'  7  4
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  Trivial)

---

Home Index