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:
\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
(Auto THEN Unfold `classrel` 0 THEN Auto)
Home
Index