---

Step * of Lemma once-once-class

∀[Info,A:Type]. ∀[X:EClass(A)].  (((X once) once) = (X once) ∈ EClass(A))
BY
{ (RepUR ``once-class`` 0
   THEN Auto
   THEN RW (AddrC [2] UnfoldTopAbC) 0
   THEN Unfold `eclass` 0
   THEN RepeatFor 2 (((BetterExt THENM (Reduce 0 THEN Auto))
                      THENA (Auto THEN RepUR ``until-class`` 0 THEN Auto THEN Auto)
                      ))) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. es : EO+(Info)@i'
5. e : E@i
⊢ case class-pred((X until X);es;e) of inl(e') => {} | inr(z) => (X until X) es e = ((X until X) es e) ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].    (((X  once)  once)  =  (X  once))


By

---

Latex:
(RepUR  ``once-class``  0
  THEN  Auto
  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
  THEN  Unfold  `eclass`  0
  THEN  RepeatFor  2  (((BetterExt  THENM  (Reduce  0  THEN  Auto))
                                        THENA  (Auto  THEN  RepUR  ``until-class``  0  THEN  Auto  THEN  Auto)
                                        )))

---

Home Index