---

Step * 2 2 1 of Lemma split_tail_trivial

.....falsecase..... 
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀b:A. ((b ∈ [u / v]) ⇒ (↑f[b]))
6. split_tail(v | ∀x.f[x]) = <[], v> ∈ (A List × (A List))
7. ¬↑f[u]
⊢ <[u], v> = <[], [u / v]> ∈ (A List × (A List))
BY
{ ((D (-1) THEN BackThruSomeHyp) THENA Auto) }

1
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀b:A. ((b ∈ [u / v]) ⇒ (↑f[b]))
6. split_tail(v | ∀x.f[x]) = <[], v> ∈ (A List × (A List))
⊢ (u ∈ [u / v])

---

Latex:

---

Latex:
.....falsecase..... 
1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \mforall{}b:A.  ((b  \mmember{}  [u  /  v])  {}\mRightarrow{}  (\muparrow{}f[b]))
6.  split\_tail(v  |  \mforall{}x.f[x])  =  <[],  v>
7.  \mneg{}\muparrow{}f[u]
\mvdash{}  <[u],  v>  =  <[],  [u  /  v]>


By

---

Latex:
((D  (-1)  THEN  BackThruSomeHyp)  THENA  Auto)

---

Home Index