---

Step * of Lemma es-E-interface-first

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[Ias:EClass(A) List]. ∀[i:ℕ||Ias||].  (E(Ias[i]) ⊆r E(first-eclass(Ias)))
BY
{ (Auto
   THEN BLemma `es-E-interface_functionality` 
   THEN Auto
   THEN RWO "es-is-interface-p-first" 0
   THEN Auto
   THEN Using [`A',⌈A⌉] Auto⋅) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. Ias : EClass(A) List
5. i : ℕ||Ias||
6. e : E@i
7. ↑e ∈b Ias[i]@i
⊢ (∃I∈Ias. ↑e ∈b I)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[Ias:EClass(A)  List].  \mforall{}[i:\mBbbN{}||Ias||].
    (E(Ias[i])  \msubseteq{}r  E(first-eclass(Ias)))


By

---

Latex:
(Auto
  THEN  BLemma  `es-E-interface\_functionality` 
  THEN  Auto
  THEN  RWO  "es-is-interface-p-first"  0
  THEN  Auto
  THEN  Using  [`A',\mkleeneopen{}A\mkleeneclose{}]  Auto\mcdot{})

---

Home Index