---

Step * of Lemma list_split_inverse

∀[T:Type]. ∀[f:(T List) ⟶ 𝔹]. ∀[L:T List]. ∀[LL:T List List]. ∀[X:T List].
  L = (concat(LL) @ X) ∈ (T List) supposing list_split(f;L) = <LL, X> ∈ (T List List × (T List))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;2]
   THEN Auto
   THEN D -3
   THEN D -4
   THEN All Reduce
   THEN AutoSimpHyp Auto (-1)
   THEN D -4
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:(T  List)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].  \mforall{}[LL:T  List  List].  \mforall{}[X:T  List].
    L  =  (concat(LL)  @  X)  supposing  list\_split(f;L)  =  <LL,  X>


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;2]
  THEN  Auto
  THEN  D  -3
  THEN  D  -4
  THEN  All  Reduce
  THEN  AutoSimpHyp  Auto  (-1)
  THEN  D  -4
  THEN  Auto)

---

Home Index