---

Step * of Lemma implies-equiv-props

∀L:ℙ List+. ((∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])) ⇒ (last(L) ⇒ hd(L)) ⇒ equiv-props(L))
BY
{ Auto }

1
1. L : ℙ List+
2. ∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])
3. last(L) ⇒ hd(L)
⊢ equiv-props(L)

---

Latex:

---

Latex:
\mforall{}L:\mBbbP{}  List\msupplus{}.  ((\mforall{}i:\mBbbN{}||L||  -  1.  (L[i]  {}\mRightarrow{}  L[i  +  1]))  {}\mRightarrow{}  (last(L)  {}\mRightarrow{}  hd(L))  {}\mRightarrow{}  equiv-props(L))


By

---

Latex:
Auto

---

Home Index