---

Step * 1 of Lemma list_split_one_one


1. T : Type
2. f : (T List) ⟶ 𝔹
3. X : T List
4. Y : T List
5. list_split(f;X) = list_split(f;Y) ∈ (T List List × (T List))
6. X = (concat(fst(list_split(f;X))) @ (snd(list_split(f;X)))) ∈ (T List)
7. Y = (concat(fst(list_split(f;Y))) @ (snd(list_split(f;Y)))) ∈ (T List)
⊢ X = Y ∈ (T List)
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  X  :  T  List
4.  Y  :  T  List
5.  list\_split(f;X)  =  list\_split(f;Y)
6.  X  =  (concat(fst(list\_split(f;X)))  @  (snd(list\_split(f;X))))
7.  Y  =  (concat(fst(list\_split(f;Y)))  @  (snd(list\_split(f;Y))))
\mvdash{}  X  =  Y


By

---

Latex:
xxxAutoxxx

---

Home Index