---

Step * of Lemma accessible-iff

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[t:T].  (accessible(T;x,y.R[x;y];t) ⇐⇒ ∀u:T. (R[u;t] ⇒ accessible(T;x,y.R[x;y];u)))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN (D 0 THENA Auto) THEN All (Unfold `accessible`)) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [t] : T
4. pW t@i
⊢ ∀u:T. (R[u;t] ⇒ (pW u))

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [t] : T
4. ∀u:T. (R[u;t] ⇒ (pW u))@i
⊢ pW t

---

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{}u:T.  (R[u;t]  {}\mRightarrow{}  accessible(T;x,y.R[x;y];u)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0  THEN  (D  0  THENA  Auto)  THEN  All  (Unfold  `accessible`))

---

Home Index