---

Step * 2 2 of Lemma split-at-first


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. u : T
5. v : T List
6. X : T List
7. Y : T List
8. v = (X @ Y) ∈ (T List)
9. (∀x∈X.¬P[x])
10. P[hd(Y)] supposing ||Y|| ≥ 1 
11. ¬P[u]
⊢ ∃X,Y:T List. (([u / v] = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )
BY
{ (InstConcl [⌜[u / X]⌝;⌜Y⌝]⋅ THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(P[x])
4.  u  :  T
5.  v  :  T  List
6.  X  :  T  List
7.  Y  :  T  List
8.  v  =  (X  @  Y)
9.  (\mforall{}x\mmember{}X.\mneg{}P[x])
10.  P[hd(Y)]  supposing  ||Y||  \mgeq{}  1 
11.  \mneg{}P[u]
\mvdash{}  \mexists{}X,Y:T  List.  (([u  /  v]  =  (X  @  Y))  \mwedge{}  (\mforall{}x\mmember{}X.\mneg{}P[x])  \mwedge{}  P[hd(Y)]  supposing  ||Y||  \mgeq{}  1  )


By

---

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

---

Home Index