---

Step * of Lemma bind-class_wf

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:A ─→ EClass(B)].  (X >x> Y[x] ∈ EClass(B))
BY
{ (Auto
   THEN RepUR ``eclass bind-class`` 0
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN (GenConcl ⌈≤loc(e) = L ∈ bag({e':E| e' ≤loc e } )⌉⋅ THEN Auto⋅)⋅) }

---

Latex:


\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(B)].    (X  >x>  Y[x]  \mmember{}  EClass(B))


By

(Auto
  THEN  RepUR  ``eclass  bind-class``  0
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}\mleq{}loc(e)  =  L\mkleeneclose{}\mcdot{}  THEN  Auto\mcdot{})\mcdot{})

---

Home Index