---

Step * of Lemma fun-connected-relation

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:E(X) ⟶ E(X).
    ∀[R:E(X) ⟶ E(X) ⟶ ℙ]
      (Trans(E(X);e',e.R[e';e])
      ⇒ Refl(E(X);e',e.R[e';e])
      ⇒ (∀x:E(X). R[f x;x])
      ⇒ (∀e',e:E(X).  (e' is f*(e) ⇒ R[e';e])))
BY
{ (RepeatFor 8 ((D 0 THENA Auto)) THEN BLemma `fun-connected-induction` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E(X).
        \mforall{}[R:E(X)  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}]
            (Trans(E(X);e',e.R[e';e])
            {}\mRightarrow{}  Refl(E(X);e',e.R[e';e])
            {}\mRightarrow{}  (\mforall{}x:E(X).  R[f  x;x])
            {}\mRightarrow{}  (\mforall{}e',e:E(X).    (e'  is  f*(e)  {}\mRightarrow{}  R[e';e])))


By

---

Latex:
(RepeatFor  8  ((D  0  THENA  Auto))  THEN  BLemma  `fun-connected-induction`  THEN  Auto)

---

Home Index