---

Step * of Lemma es-info_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e:E].  (info(e) ∈ Info)
BY
{ (Auto
   THEN (Assert e ∈ es-base-E(es) BY
               (DVar `e' THEN All (Fold `es-base-E`) THEN Trivial))
   THEN ProveWfLemma
   THEN DVar `es'⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (info(e)  \mmember{}  Info)


By

(Auto
  THEN  (Assert  e  \mmember{}  es-base-E(es)  BY
                          (DVar  `e'  THEN  All  (Fold  `es-base-E`)  THEN  Trivial))
  THEN  ProveWfLemma
  THEN  DVar  `es'\mcdot{}
  THEN  Auto)

---

Home Index