---

Step * of Lemma least-equiv-induction2

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀x,y:A.  ((x least-equiv(A;R) y) ⇒ {∀[P:A ⟶ ℙ]. ((∀x,y:A.  ((x R y) ⇒ (P[x] ⇐⇒ P[y]))) ⇒ P[x] ⇒ P[y])})
BY
{ (Auto THEN D 0 THEN Auto THEN InstLemma `least-equiv-induction` [⌜A⌝;⌜P⌝;⌜R⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,y:A.
        ((x  least-equiv(A;R)  y)
        {}\mRightarrow{}  \{\mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x,y:A.    ((x  R  y)  {}\mRightarrow{}  (P[x]  \mLeftarrow{}{}\mRightarrow{}  P[y])))  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y])\})


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  InstLemma  `least-equiv-induction`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index