---

Step * 1 of Lemma es-interface-val-disjoint


1. Info : Type
2. es : EO+(Info)
3. A : Type
4. Xs : EClass(A) List
5. ∀X:EClass(A). ((X ∈ Xs) ⇒ (∀Y:EClass(A). ((Y ∈ Xs) ⇒ ((X = Y ∈ EClass(A)) ∨ X ∩ Y = 0))))
6. X : EClass(A)
7. (X ∈ Xs)
8. e : E
9. ↑e ∈b X
10. ↑e ∈b first-eclass(Xs)
⊢ first-eclass(Xs)(e) = X(e) ∈ A
BY
{ ((FLemma `first-eclass-val` [-1]⋅ THEN Auto)
   THEN D -1
   THEN Auto
   THEN NthHypEq (-1)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
2:n
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. Xs : EClass(A) List
5. ∀X:EClass(A). ((X ∈ Xs) ⇒ (∀Y:EClass(A). ((Y ∈ Xs) ⇒ ((X = Y ∈ EClass(A)) ∨ X ∩ Y = 0))))
6. X : EClass(A)
7. (X ∈ Xs)
8. e : E
9. ↑e ∈b X
10. ↑e ∈b first-eclass(Xs)
11. i : ℕ||Xs||
12. ↑e ∈b Xs[i]
13. first-eclass(Xs)(e) = Xs[i](e) ∈ A
⊢ X = Xs[i] ∈ EClass(A)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  Xs  :  EClass(A)  List
5.  \mforall{}X:EClass(A).  ((X  \mmember{}  Xs)  {}\mRightarrow{}  (\mforall{}Y:EClass(A).  ((Y  \mmember{}  Xs)  {}\mRightarrow{}  ((X  =  Y)  \mvee{}  X  \mcap{}  Y  =  0))))
6.  X  :  EClass(A)
7.  (X  \mmember{}  Xs)
8.  e  :  E
9.  \muparrow{}e  \mmember{}\msubb{}  X
10.  \muparrow{}e  \mmember{}\msubb{}  first-eclass(Xs)
\mvdash{}  first-eclass(Xs)(e)  =  X(e)


By

---

Latex:
((FLemma  `first-eclass-val`  [-1]\mcdot{}  THEN  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index