---

Step * of Lemma es-fset-at_wf

∀[es:EO]. ∀[i:Id]. ∀[s:fset(E)].  (s@i ∈ E List)
BY
{ (Auto THEN Unfold `es-fset-at` 0) }

1
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

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[s:fset(E)].    (s@i  \mmember{}  E  List)


By

---

Latex:
(Auto  THEN  Unfold  `es-fset-at`  0)

---

Home Index