---

Step * of Lemma locknd-spread_wf

∀[T:i:Id ─→ k:{k:Knd| ↑hasloc(k;i)}  ─→ Type]. ∀[P:i:Id ─→ k:{k:Knd| ↑hasloc(k;i)}  ─→ T[i;k]]. ∀[ik:LocKnd].
  (let i,k:LocKnd = ik in P[i;k] ∈ T[fst(ik);snd(ik)])
BY
{ (Unfolds ``LocKnd locknd-spread`` 0
   THEN RepeatFor 3 (((D 0 THENA Try (Complete (Auto))) THEN Try ((RepeatFor 2 (DVar `ik') THEN All Reduce THEN Auto))))
   ) }

---

Latex:


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


By

(Unfolds  ``LocKnd  locknd-spread``  0
  THEN  RepeatFor  3  (((D  0  THENA  Try  (Complete  (Auto)))
                                        THEN  Try  ((RepeatFor  2  (DVar  `ik')  THEN  All  Reduce  THEN  Auto))
                                        ))
  )

---

Home Index