---

Step * 1 of Lemma es-decl-set-single_wf


1. i : Id
2. ds : x:Id fp-> Type
3. da : k:{k:Knd| ↑hasloc(k;i)}  fp-> Type
4. ∀i@0:Id. ((i@0 ∈ [i]) ∈ Type)
5. i1 : Id@i
6. (i1 ∈ [i])@i
⊢ da ∈ k:{k:Knd| ↑hasloc(k;i1)}  fp-> Type
BY
{ ((RWO  "member_singleton" (-1) THENA Auto) THEN HypSubst' -1 0 THEN Auto) }

---

Latex:



1.  i  :  Id
2.  ds  :  x:Id  fp->  Type
3.  da  :  k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    fp->  Type
4.  \mforall{}i@0:Id.  ((i@0  \mmember{}  [i])  \mmember{}  Type)
5.  i1  :  Id@i
6.  (i1  \mmember{}  [i])@i
\mvdash{}  da  \mmember{}  k:\{k:Knd|  \muparrow{}hasloc(k;i1)\}    fp->  Type


By

((RWO    "member\_singleton"  (-1)  THENA  Auto)  THEN  HypSubst'  -1  0  THEN  Auto)

---

Home Index