---

Step * of Lemma decidable__classrel

∀[Info,T:Type].  ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀X:EClass(T). ∀es:EO+(Info). ∀e:E. ∀v:T.  Dec(v ∈ X(e))))
BY
{ (Auto THEN Unfold `classrel` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].
    ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}v:T.    Dec(v  \mmember{}  X(e))))


By

---

Latex:
(Auto  THEN  Unfold  `classrel`  0  THEN  Auto)

---

Home Index