---

Step * of Lemma bar-converges_functionality

∀[T:Type]. ∀[x,y:bar-base(T)]. ∀[a:T].  (bar-equal(T;x;y) ⇒ {x↓a ⇐⇒ x↓a})
BY
{ (Unfold `guard` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index