---

Step * of Lemma split_tail_wf

∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].  (split_tail(L | ∀x.f[x]) ∈ A List × (A List))
BY
{ ((((Auto THEN ListInd (-1)) THEN RecUnfold `split_tail` 0) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].    (split\_tail(L  |  \mforall{}x.f[x])  \mmember{}  A  List  \mtimes{}  (A  List))


By

---

Latex:
((((Auto  THEN  ListInd  (-1))  THEN  RecUnfold  `split\_tail`  0)  THEN  Reduce  0)  THEN  Auto)

---

Home Index