---

Step * of Lemma es-pred_wf

∀[the_es:EO]. ∀[e:E].  pred(e) ∈ E supposing ¬↑first(e)
BY
{ (Auto
   THEN Unfold `es-E` 0
   THEN Folds ``es-base-E es-dom`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Try ((BLemma `es-pred-wf-base` THEN Auto))) }

1
.....set predicate..... 
1. the_es : EO
2. e : E
3. ¬↑first(e)
⊢ ↑(es-dom(the_es) pred(e))

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e:E].    pred(e)  \mmember{}  E  supposing  \mneg{}\muparrow{}first(e)


By

(Auto
  THEN  Unfold  `es-E`  0
  THEN  Folds  ``es-base-E  es-dom``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((BLemma  `es-pred-wf-base`  THEN  Auto)))

---

Home Index