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