---

Step * 1 1 2 of Lemma eo-restrict_property

.....set predicate..... 
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. x : es-base-E(es)@i
4. ↑((es-dom(es) x) ∧b (P x))@i
⊢ ↑(P x)
BY
{ (MoveToConcl (-1)
   THEN (BoolCase ⌈es-dom(es) x⌉⋅ THENA Auto)
   THEN Auto
   THEN MemTypeCD
   THEN Folds ``es-base-E es-dom`` 0
   THEN Auto) }

---

Latex:


.....set  predicate..... 
1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}@i
3.  x  :  es-base-E(es)@i
4.  \muparrow{}((es-dom(es)  x)  \mwedge{}\msubb{}  (P  x))@i
\mvdash{}  \muparrow{}(P  x)


By

(MoveToConcl  (-1)
  THEN  (BoolCase  \mkleeneopen{}es-dom(es)  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  MemTypeCD
  THEN  Folds  ``es-base-E  es-dom``  0
  THEN  Auto)

---

Home Index