---

Step * of Lemma decidable__equal_rc

∀k:ℕ. ∀x,y:ℚCube(k).  Dec(x = y ∈ ℚCube(k))
BY
{ ((D 0 THENA Auto) THEN InstLemma `deq-implies` [⌜ℚCube(k)⌝]⋅ THEN Auto THEN UseWitness ⌜rc-deq(k)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}x,y:\mBbbQ{}Cube(k).    Dec(x  =  y)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  InstLemma  `deq-implies`  [\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  UseWitness  \mkleeneopen{}rc-deq(k)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index