---

Step * 1 of Lemma subtype-set-hasloc


1. i : Id
2. d : {k:Knd| ↑hasloc(k;i)}  List
3. k : Knd@i
4. (k ∈ d)@i
⊢ ↑hasloc(k;i)
BY
{ (RepeatFor 2 (D -1) THEN HypSubst' (-1) 0 THEN GenConclAtAddr [1;1] THEN DVar `v' THEN Auto) }

---

Latex:



1.  i  :  Id
2.  d  :  \{k:Knd|  \muparrow{}hasloc(k;i)\}    List
3.  k  :  Knd@i
4.  (k  \mmember{}  d)@i
\mvdash{}  \muparrow{}hasloc(k;i)


By

(RepeatFor  2  (D  -1)  THEN  HypSubst'  (-1)  0  THEN  GenConclAtAddr  [1;1]  THEN  DVar  `v'  THEN  Auto)

---

Home Index