---

Step * of Lemma geo-length-equiv

∀e:BasicGeometry. EquivRel({p:Point| O_X_p} ;x,y.x ≡ y)
BY
{ ((D 0 THENA Auto) THEN RepeatFor 9 ((AutoIsType ORELSE (RelRST THEN Auto) ORELSE (D 0 THEN Reduce 0) ORELSE Auto))) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  EquivRel(\{p:Point|  O\_X\_p\}  ;x,y.x  \mequiv{}  y)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepeatFor  9  ((AutoIsType  ORELSE  (RelRST  THEN  Auto)  ORELSE  (D  0  THEN  Reduce  0)  ORELSE  Auto))
  )

---

Home Index