---

Step * 2 of Lemma no-classrel-iff-empty


1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. (X es e) = {} ∈ bag(T)
7. v : T@i
⊢ ¬v ∈ X(e)
BY
{ ((D 0 THEN Auto)
   THEN RepUR ``classrel`` -1
   THEN HypSubst' -3 -1
   THEN Auto
   THEN FLemma `bag-member-empty` [-1]
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  es  :  EO+(Info)
5.  e  :  E
6.  (X  es  e)  =  \{\}
7.  v  :  T@i
\mvdash{}  \mneg{}v  \mmember{}  X(e)


By

((D  0  THEN  Auto)
  THEN  RepUR  ``classrel``  -1
  THEN  HypSubst'  -3  -1
  THEN  Auto
  THEN  FLemma  `bag-member-empty`  [-1]
  THEN  Auto)

---

Home Index