---

Step * 1 of Lemma split-at-first


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 )
BY
{ (InstConcl [⌜[]⌝;⌜[]⌝]⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(InstConcl  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index