---

Step * 1 of Lemma es-fset-at_wf


1. es : EO
2. i : Id
3. s : fset(E)
⊢ fst((TERMOF{es-fset-at-loc:o, 1:l, i:l} es i s)) ∈ E List
BY
{ ((GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0) THEN Auto) }

---

Latex:



1.  es  :  EO
2.  i  :  Id
3.  s  :  fset(E)
\mvdash{}  fst((TERMOF\{es-fset-at-loc:o,  1:l,  i:l\}  es  i  s))  \mmember{}  E  List


By

((GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0)  THEN  Auto)

---

Home Index