---

Step * of Lemma es-le-interface_wf

∀[Info,A:Type]. ∀[X:EClass(A)].  (le(X) ∈ EClass(E(X)))
BY
{ (ProveWfLemma
   THEN SubsumeC ⌜EClass({e:E| ↑((λes,e. e ∈b X) es e)} )⌝⋅
   THEN Auto
   THEN Reduce 0
   THEN Fold `es-E-interface` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].    (le(X)  \mmember{}  EClass(E(X)))


By

---

Latex:
(ProveWfLemma
  THEN  SubsumeC  \mkleeneopen{}EClass(\{e:E|  \muparrow{}((\mlambda{}es,e.  e  \mmember{}\msubb{}  X)  es  e)\}  )\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  Fold  `es-E-interface`  0
  THEN  Auto)

---

Home Index