---

Step * of Lemma parallel-class-zero

∀[T,Info:Type]. ∀[X:EClass(T)].  (X || Empty = X ∈ EClass(T))
BY
{ (Auto
   THEN RepUR ``eclass`` 0
   THEN ((Ext THEN Auto) THEN RenameVar `es' (-1) THEN Reduce 0)
   THEN (Ext THEN Auto)
   THEN RenameVar `e' (-1)
   THEN Reduce 0) }

1
1. T : Type
2. Info : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
⊢ (X || Empty es e) = (X es e) ∈ bag(T)

---

Latex:


\mforall{}[T,Info:Type].  \mforall{}[X:EClass(T)].    (X  ||  Empty  =  X)


By

(Auto
  THEN  RepUR  ``eclass``  0
  THEN  ((Ext  THEN  Auto)  THEN  RenameVar  `es'  (-1)  THEN  Reduce  0)
  THEN  (Ext  THEN  Auto)
  THEN  RenameVar  `e'  (-1)
  THEN  Reduce  0)

---

Home Index