Step
*
1
of Lemma
decidable__equal-int_seg
.....decidable?.....
1. [a] : ℤ
2. [b] : ℤ
3. x : {a..b-}
4. y : {a..b-}
5. x = y ∈ ℤ
⊢ Dec(x = y ∈ {a..b-})
BY
{ ((OrLeft THENA Auto) THEN EqTypeCD THEN Auto) }
Latex:
Latex:
.....decidable?.....
1. [a] : \mBbbZ{}
2. [b] : \mBbbZ{}
3. x : \{a..b\msupminus{}\}
4. y : \{a..b\msupminus{}\}
5. x = y
\mvdash{} Dec(x = y)
By
Latex:
((OrLeft THENA Auto) THEN EqTypeCD THEN Auto)
Home
Index