---

Step * 1 of Lemma list_split_prefix


1. T : Type
⊢ ∀[g:(T List) ⟶ 𝔹]. ↑(g (snd(list_split(g;concat(fst(list_split(g;[]))))))) supposing ¬↑null(fst(list_split(g;[])))
BY
{ (Unfold `list_split` 0 THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  \mforall{}[g:(T  List)  {}\mrightarrow{}  \mBbbB{}]
        \muparrow{}(g  (snd(list\_split(g;concat(fst(list\_split(g;[])))))))  supposing  \mneg{}\muparrow{}null(fst(list\_split(g;[])))


By

---

Latex:
(Unfold  `list\_split`  0  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index