---

Step * of Lemma decidable__equal_rationals

∀r,s:ℚ.  Dec(r = s ∈ ℚ)
BY
{ xxx(Auto THEN UseWitness ⌜if qeq(r;s) then inl ⋅ else inr (λx.⋅)  fi ⌝⋅)xxx }

1
1. r : ℚ
2. s : ℚ
⊢ if qeq(r;s) then inl ⋅ else inr (λx.⋅)  fi  ∈ Dec(r = s ∈ ℚ)

---

Latex:

---

Latex:
\mforall{}r,s:\mBbbQ{}.    Dec(r  =  s)


By

---

Latex:
xxx(Auto  THEN  UseWitness  \mkleeneopen{}if  qeq(r;s)  then  inl  \mcdot{}  else  inr  (\mlambda{}x.\mcdot{})    fi  \mkleeneclose{}\mcdot{})xxx

---

Home Index