---

Step * of Lemma but-first-class_wf

∀[Info,A:Type]. ∀[X:EClass(A)].  (Skip-e(X) ∈ EClass(A))
BY
{ ((Auto THEN Unfolds ``eclass but-first-class`` 0)
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN (BoolCase ⌜first(e)⌝⋅ THENA Auto)) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. es : EO+(Info)@i'
5. e : E@i
6. ↑first(e)
⊢ {} ∈ bag(A)

2
1. Info : Type
2. A : Type
3. X : EClass(A)
4. es : EO+(Info)@i'
5. e : E@i
6. ¬↑first(e)
⊢ X es>es-init(es;e) e ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].    (Skip-e(X)  \mmember{}  EClass(A))


By

---

Latex:
((Auto  THEN  Unfolds  ``eclass  but-first-class``  0)
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  (BoolCase  \mkleeneopen{}first(e)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index