---

Step * 1 of Lemma bind-zero-left


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)
BY
{ (RepUR ``es-empty-interface bind-class eclass-bag-val in-eclass`` 0
   THEN RenameVar `e' (-1)
   THEN GenConcl ⌈≤loc(e) = B ∈ bag({e':E| e' ≤loc e } )⌉⋅
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  S  :  Type
4.  f  :  T  {}\mrightarrow{}  EClass(S)@i'
5.  \mforall{}[X:EClass(T)].  \mforall{}[Y:T  {}\mrightarrow{}  EClass(S)].    (X  >x>  Y[x]  \mmember{}  EClass(S))
6.  Empty  \mmember{}  EClass(T)
7.  es  :  EO+(Info)
8.  x  :  E
\mvdash{}  (Empty  es  x)  =  (Empty  >z>  f[z]  es  x)


By

(RepUR  ``es-empty-interface  bind-class  eclass-bag-val  in-eclass``  0
  THEN  RenameVar  `e'  (-1)
  THEN  GenConcl  \mkleeneopen{}\mleq{}loc(e)  =  B\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index