---

Step * of Lemma is-first-class

∀[Info,A:Type].  ∀L:EClass(A) List. ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-class(L) ⇐⇒ (∃X∈L. ↑e ∈b X))
BY
{ (InductionOnList
   THEN Unfold `first-class` 0
   THEN Reduce 0
   THEN Try ((Fold `first-class` 0 THEN RepeatFor 2 (ParallelLast)))) }

1
1. [Info] : Type
2. [A] : Type
⊢ ∀es:EO+(Info). ∀e:E.  (False ⇐⇒ (∃X∈[]. ↑e ∈b X))

2
1. [Info] : Type
2. [A] : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-class(v) ⇐⇒ (∃X∈v. ↑e ∈b X))@i'
6. es : EO+(Info)@i'
7. ∀e:E. (↑e ∈b first-class(v) ⇐⇒ (∃X∈v. ↑e ∈b X))
8. e : E@i
9. ↑e ∈b first-class(v) ⇐⇒ (∃X∈v. ↑e ∈b X)
⊢ ↑e ∈b [u?first-class(v)] ⇐⇒ (∃X∈[u / v]. ↑e ∈b X)

---

Latex:


\mforall{}[Info,A:Type].    \mforall{}L:EClass(A)  List.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  first-class(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}L.  \muparrow{}e  \mmember{}\msubb{}  X))


By

(InductionOnList
  THEN  Unfold  `first-class`  0
  THEN  Reduce  0
  THEN  Try  ((Fold  `first-class`  0  THEN  RepeatFor  2  (ParallelLast))))

---

Home Index