---

Step * of Lemma bind-zero-left

∀[Info,T,S:Type].  ∀f:T ─→ EClass(S). (Empty >z> f[z] = Empty ∈ EClass(S))
BY
{ ((Auto THEN (InstLemma `bind-class_wf` [⌈Info⌉;⌈T⌉;⌈S⌉]⋅ THENA 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 RenameVar `es' (-1)⋅
   THEN Ext
   THEN Try (Complete (Auto))) }

1
1. Info : Type
2. T : Type
3. S : Type
4. f : T ─→ EClass(S)@i'
5. ∀[X:EClass(T)]. ∀[Y:T ─→ EClass(S)].  (X >x> Y[x] ∈ EClass(S))
6. Empty ∈ EClass(T)
7. es : EO+(Info)
8. x : E
⊢ (Empty es x) = (Empty >z> f[z] es x) ∈ bag(S)

---

Latex:


\mforall{}[Info,T,S:Type].    \mforall{}f:T  {}\mrightarrow{}  EClass(S).  (Empty  >z>  f[z]  =  Empty)


By

((Auto  THEN  (InstLemma  `bind-class\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{}  THENA  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  \mcdot{}  THEN  Auto)\mcdot{})
  THEN  RenameVar  `es'  (-1)\mcdot{}
  THEN  Ext
  THEN  Try  (Complete  (Auto)))

---

Home Index