---

Step * of Lemma has-latest-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[e:E].  ↑e ∈b (X)- supposing (↑e ∈b X) ∨ (↑e ∈b (X)')
BY
{ Auto
THEN Unfold `in-eclass` 0
THEN RepUR ``es-latest-val`` 0
THEN SplitOnConclITE
THEN Reduce 0
THEN Auto }

1
1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. e : E
6. (↑e ∈b X) ∨ (↑e ∈b (X)')
7. ¬↑e ∈b X
⊢ #((X)' es e) = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[e:E].
    \muparrow{}e  \mmember{}\msubb{}  (X)\msupminus{}  supposing  (\muparrow{}e  \mmember{}\msubb{}  X)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  (X)')


By

---

Latex:
Auto
THEN  Unfold  `in-eclass`  0
THEN  RepUR  ``es-latest-val``  0
THEN  SplitOnConclITE
THEN  Reduce  0
THEN  Auto

---

Home Index