---

Step * of Lemma es-interface-val_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[e:E].  X(e) ∈ A supposing ↑e ∈b X
BY
{ (Unfolds ``in-eclass eclass-val eclass`` 0
   THEN Auto
   THEN OnMaybeHyp 6 (\h. (RW assert_pushdownC h THEN Complete (EAuto 1)))) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].    X(e)  \mmember{}  A  supposing  \muparrow{}e  \mmember{}\msubb{}  X


By

(Unfolds  ``in-eclass  eclass-val  eclass``  0
  THEN  Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (RW  assert\_pushdownC  h  THEN  Complete  (EAuto  1))))

---

Home Index