---

Step * 1 1 of Lemma locl-pre-preserving-1-1


1. es : EO
2. P : E ─→ ℙ
3. f : {e:E| P e}  ─→ E
4. f is λe,e'. e ≤loc e' -λe,e'. e ≤loc e' -pre-preserving on P
⊢ Refl(E;e,e'.e ≤loc e' )
BY
{ (Unfold `refl` 0 THEN Auto) }

---

Latex:



1.  es  :  EO
2.  P  :  E  {}\mrightarrow{}  \mBbbP{}
3.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  E
4.  f  is  \mlambda{}e,e'.  e  \mleq{}loc  e'  -\mlambda{}e,e'.  e  \mleq{}loc  e'  -pre-preserving  on  P
\mvdash{}  Refl(E;e,e'.e  \mleq{}loc  e'  )


By

(Unfold  `refl`  0  THEN  Auto)

---

Home Index