---

Step * of Lemma es-local-pred-iff-es-p-local-pred

∀[Info,T:Type].
  ∀X:EClass(T). ∀es:EO+(Info). ∀e,e':E.
    uiff((last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top);es-p-local-pred(es;λe'.inhabited-classrel(es;T;X;e')) e 
                                                              e')
BY
{ ((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA (Auto THEN Reduce 0 THEN Auto))) }

1
1. [Info] : Type
2. [T] : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. e : E@i
6. e' : E@i
7. (last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top)
⊢ es-p-local-pred(es;λe'.inhabited-classrel(es;T;X;e')) e e'

2
1. Info : Type
2. T : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. e : E@i
6. e' : E@i
7. es-p-local-pred(es;λe'.inhabited-classrel(es;T;X;e')) e e'
⊢ (last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top)

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].
    \mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e,e':E.
        uiff((last(\mlambda{}e'.0  <z  \#(X  es  e'))  e)
        =  (inl  e');es-p-local-pred(es;\mlambda{}e'.inhabited-classrel(es;T;X;e'))  e  e')


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  (Auto  THEN  Reduce  0  THEN  Auto)))

---

Home Index