---

Step * of Lemma accessible-inversion

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[u:T].  ∀v:T. (accessible(T;x,y.R[x;y];u) ⇒ R[v;u] ⇒ accessible(T;x,y.R[x;y];v))
BY
{ ((InstLemma `accessible-iff` [] THEN RepeatFor 3 (ParallelLast')) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[u:T].
    \mforall{}v:T.  (accessible(T;x,y.R[x;y];u)  {}\mRightarrow{}  R[v;u]  {}\mRightarrow{}  accessible(T;x,y.R[x;y];v))


By

---

Latex:
((InstLemma  `accessible-iff`  []  THEN  RepeatFor  3  (ParallelLast'))  THEN  Auto)

---

Home Index