Step
*
of Lemma
streamless-dec-equal
∀[T:Type]. (streamless(T)
⇒ (∀x,y:T. Dec(x = y ∈ T)))
BY
{ xxxAutoxxx }
1
.....decidable?.....
1. [T] : Type
2. streamless(T)
3. x : T
4. y : T
⊢ Dec(x = y ∈ T)
Latex:
Latex:
\mforall{}[T:Type]. (streamless(T) {}\mRightarrow{} (\mforall{}x,y:T. Dec(x = y)))
By
Latex:
xxxAutoxxx
Home
Index