---

Step * of Lemma bind-zero-right

∀[Info,T:Type]. ∀[X:EClass(T)].  (X >x> Empty = Empty ∈ EClass(T))
BY
{ ((Auto THEN (Assert Empty ∈ EClass(T) BY Auto))
   THEN RepUR ``eclass`` 0⋅
   THEN Symmetry
   THEN Ext
   THEN Auto
   THEN Try ((Fold `eclass` 0 THEN Auto THEN SubsumeC ⌈EClass(T)⌉⋅ THEN Auto))
   THEN RenameVar `es' (-1)⋅
   THEN Ext
   THEN Auto) }

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

---

Latex:


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


By

((Auto  THEN  (Assert  Empty  \mmember{}  EClass(T)  BY  Auto))
  THEN  RepUR  ``eclass``  0\mcdot{}
  THEN  Symmetry
  THEN  Ext
  THEN  Auto
  THEN  Try  ((Fold  `eclass`  0  THEN  Auto  THEN  SubsumeC  \mkleeneopen{}EClass(T)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RenameVar  `es'  (-1)\mcdot{}
  THEN  Ext
  THEN  Auto)

---

Home Index