---

Step * of Lemma assert-rceq

∀[k:ℕ]. ∀[a,b:ℚCube(k)].  uiff(↑rceq(k;a;b);a = b ∈ ℚCube(k))
BY
{ ((D 0 THENA Auto)
   THEN RepUR ``rceq`` 0
   THEN GenConclTerm ⌜rc-deq(k)⌝⋅
   THEN Auto
   THEN D 2
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[a,b:\mBbbQ{}Cube(k)].    uiff(\muparrow{}rceq(k;a;b);a  =  b)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepUR  ``rceq``  0
  THEN  GenConclTerm  \mkleeneopen{}rc-deq(k)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  2
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index