---

Step * 1 of Lemma sub-es-pred_wf


∀es:EO. ∀dom:E ─→ 𝔹. ∀e:E.  (sub-es-pred(es;dom;e) ∈ {e:E| ↑(dom e)} ?)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN StrongLocLessInd THEN RecUnfold `sub-es-pred` 0 THEN SplitOnConclITE THEN Auto) }

---

Latex:



\mforall{}es:EO.  \mforall{}dom:E  {}\mrightarrow{}  \mBbbB{}.  \mforall{}e:E.    (sub-es-pred(es;dom;e)  \mmember{}  \{e:E|  \muparrow{}(dom  e)\}  ?)


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  StrongLocLessInd
  THEN  RecUnfold  `sub-es-pred`  0
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index