---

Step * of Lemma fun-connected-test

∀[T:Type]. ∀f:T ⟶ T. ∀x,y,z,w:T.  (y is f*(x) ⇒ z is f*(y) ⇒ w is f*(z) ⇒ w is f*(x))
BY
{ (Auto THEN RelRST THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x,y,z,w:T.    (y  is  f*(x)  {}\mRightarrow{}  z  is  f*(y)  {}\mRightarrow{}  w  is  f*(z)  {}\mRightarrow{}  w  is  f*(x))


By

---

Latex:
(Auto  THEN  RelRST  THEN  Auto)

---

Home Index