---

Step * 2 of Lemma list_split_prefix


1. T : Type
⊢ ∀ys:T List. ∀y:T.
    ((∀[g:(T List) ⟶ 𝔹]
        ↑(g (snd(list_split(g;concat(fst(list_split(g;ys))))))) supposing ¬↑null(fst(list_split(g;ys))))
    ⇒ (∀[g:(T List) ⟶ 𝔹]
          ↑(g (snd(list_split(g;concat(fst(list_split(g;ys @ [y]))))))) supposing ¬↑null(fst(list_split(g;ys @ [y])))))
BY
{ xxx(RepeatFor 3 ((D 0 THENA Auto)) THEN ParallelLast THEN (Unhide THENA Auto))xxx }

1
1. T : Type
2. ys : T List
3. y : T
4. ∀[g:(T List) ⟶ 𝔹]. ↑(g (snd(list_split(g;concat(fst(list_split(g;ys))))))) supposing ¬↑null(fst(list_split(g;ys)))
5. g : (T List) ⟶ 𝔹
6. ↑(g (snd(list_split(g;concat(fst(list_split(g;ys))))))) supposing ¬↑null(fst(list_split(g;ys)))
⊢ ↑(g (snd(list_split(g;concat(fst(list_split(g;ys @ [y]))))))) supposing ¬↑null(fst(list_split(g;ys @ [y])))

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(RepeatFor  3  ((D  0  THENA  Auto))  THEN  ParallelLast  THEN  (Unhide  THENA  Auto))xxx

---

Home Index