---

Step * of Lemma subtype-set-hasloc

∀[i:Id]. ∀[d:{k:Knd| ↑hasloc(k;i)}  List].  ({k:Knd| (k ∈ d)}  ⊆r {k:{k:Knd| ↑hasloc(k;i)} | (k ∈ d)} )
BY
{ (Auto THEN SubtypeReasoning THEN Auto) }

1
1. i : Id
2. d : {k:Knd| ↑hasloc(k;i)}  List
3. k : Knd@i
4. (k ∈ d)@i
⊢ ↑hasloc(k;i)

---

Latex:


\mforall{}[i:Id].  \mforall{}[d:\{k:Knd|  \muparrow{}hasloc(k;i)\}    List].    (\{k:Knd|  (k  \mmember{}  d)\}    \msubseteq{}r  \{k:\{k:Knd|  \muparrow{}hasloc(k;i)\}  |  (k  \mmember{}  d)\000C\}  )


By

(Auto  THEN  SubtypeReasoning  THEN  Auto)

---

Home Index