---

Step * of Lemma decidable__exists-single-valued-classrel

∀[Info,T:Type].  ∀X:EClass(T). ∀es:EO+(Info).  (single-valued-classrel(es;X;T) ⇒ (∀e:E. Dec(∃v:T. v ∈ X(e))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `single-valued-classrel` (-2)
   THEN (Assert Dec(0 < #(X es e)) BY
               Auto)
   THEN Unfold `classrel` 0
   THEN Repeat (ParallelLast)) }

1
1. [Info] : Type
2. [T] : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. ∀e:E. ∀v1,v2:T.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ T))@i
6. e : E@i
7. 0 < #(X es e)
⊢ ∃v:T. v ↓∈ X es e

2
1. Info : Type
2. T : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. ∀e:E. ∀v1,v2:T.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ T))@i
6. e : E@i
7. ∃v:T. v ↓∈ X es e@i
⊢ 0 < #(X es e)

---

Latex:


\mforall{}[Info,T:Type].
    \mforall{}X:EClass(T).  \mforall{}es:EO+(Info).    (single-valued-classrel(es;X;T)  {}\mRightarrow{}  (\mforall{}e:E.  Dec(\mexists{}v:T.  v  \mmember{}  X(e))))


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `single-valued-classrel`  (-2)
  THEN  (Assert  Dec(0  <  \#(X  es  e))  BY
                          Auto)
  THEN  Unfold  `classrel`  0
  THEN  Repeat  (ParallelLast))

---

Home Index