---

Step * of Lemma all-accessible-iff-weak-TI

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (∀t:T. accessible(T;x,y.R[x;y];t) ⇐⇒ ∀[P:T ⟶ ℙ]. weak-TI(T;x,y.R[y;x];t.P[t]))
BY
{ (InstLemma `all-accessible-iff-induction` [] THEN Fold `weak-TI` (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}t:T.  accessible(T;x,y.R[x;y];t)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  weak-TI(T;x,y.R[y;x];t.P[t]))


By

---

Latex:
(InstLemma  `all-accessible-iff-induction`  []  THEN  Fold  `weak-TI`  (-1)  THEN  Auto)

---

Home Index