---

Step * 2 of Lemma es-interface-implies-decidable


1. [Info] : Type
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : EClass(A)@i'
5. ∀e:E. Dec(∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A)))
6. e : E@i
7. ↑e ∈b X@i
⊢ ∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A))
BY
{ (InstConcl [⌈X(e)⌉]⋅ THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  A  :  Type@i'
4.  X  :  EClass(A)@i'
5.  \mforall{}e:E.  Dec(\mexists{}a:A.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e))))
6.  e  :  E@i
7.  \muparrow{}e  \mmember{}\msubb{}  X@i
\mvdash{}  \mexists{}a:A.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e)))


By

(InstConcl  [\mkleeneopen{}X(e)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index