---

Step * of Lemma bar-diverges_functionality

∀[T:Type]. ∀[x,y:bar-base(T)].  (bar-equal(T;x;y) ⇒ {x↑ ⇐⇒ y↑})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN ((RWO "bar-diverges-iff" (-1) THENA Auto)
         THEN (RWO "bar-diverges-iff" 0 THENA Auto)
         THEN ParallelLast
         THEN ParallelLast
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:bar-base(T)].    (bar-equal(T;x;y)  {}\mRightarrow{}  \{x\muparrow{}  \mLeftarrow{}{}\mRightarrow{}  y\muparrow{}\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  ((RWO  "bar-diverges-iff"  (-1)  THENA  Auto)
              THEN  (RWO  "bar-diverges-iff"  0  THENA  Auto)
              THEN  ParallelLast
              THEN  ParallelLast
              THEN  Auto)\mcdot{})

---

Home Index