---

Step * of Lemma split-at-first

∀[T:Type]. ∀[P:T ⟶ ℙ].
  ((∀x:T. Dec(P[x]))
  ⇒ (∀L:T List. ∃X,Y:T List. ((L = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )))
BY
{ xxxInductionOnListxxx }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
⊢ ∃X,Y:T List. (([] = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )

2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. u : T
5. v : T List
6. ∃X,Y:T List. ((v = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )
⊢ ∃X,Y:T List. (([u / v] = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:T.  Dec(P[x]))
    {}\mRightarrow{}  (\mforall{}L:T  List.  \mexists{}X,Y:T  List.  ((L  =  (X  @  Y))  \mwedge{}  (\mforall{}x\mmember{}X.\mneg{}P[x])  \mwedge{}  P[hd(Y)]  supposing  ||Y||  \mgeq{}  1  )))


By

---

Latex:
xxxInductionOnListxxx

---

Home Index