Step
*
1
1
of Lemma
qless-witness
.....assertion..... 
1. a : ℚ
2. b : ℚ
3. a < b
⊢ TERMOF{decidable__qless:o, 1:l} a b ∈ Dec(a < b)
BY
{ Auto }
Latex:
Latex:
.....assertion..... 
1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  a  <  b
\mvdash{}  TERMOF\{decidable\_\_qless:o,  1:l\}  a  b  \mmember{}  Dec(a  <  b)
By
Latex:
Auto
Home
Index