---

Step * 1 of Lemma decidable__equal_rationals


1. r : ℚ
2. s : ℚ
⊢ if qeq(r;s) then inl ⋅ else inr (λx.⋅)  fi  ∈ Dec(r = s ∈ ℚ)
BY
{ xxx(AutoBoolCase ⌜qeq(r;s)⌝⋅ THEN RepUR ``btrue bfalse decidable or it not`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  s  :  \mBbbQ{}
\mvdash{}  if  qeq(r;s)  then  inl  \mcdot{}  else  inr  (\mlambda{}x.\mcdot{})    fi    \mmember{}  Dec(r  =  s)


By

---

Latex:
xxx(AutoBoolCase  \mkleeneopen{}qeq(r;s)\mkleeneclose{}\mcdot{}  THEN  RepUR  ``btrue  bfalse  decidable  or  it  not``  0  THEN  Auto)xxx

---

Home Index