---

Step * 3 1 of Lemma split_tail_lemma


1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. p1 : A List
6. p2 : A List
7. ↑f[u]
⊢ ((¬↑null(p1)) ⇒ (¬↑f[last(p1)]))
⇒ (¬↑null(fst(case p1 of [] => <[], [u / p2]> | x::y => <[u / p1], p2> esac)))
⇒ (¬↑f[last(fst(case p1 of [] => <[], [u / p2]> | x::y => <[u / p1], p2> esac))])
BY
{ (ListInd (-3) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  p1  :  A  List
6.  p2  :  A  List
7.  \muparrow{}f[u]
\mvdash{}  ((\mneg{}\muparrow{}null(p1))  {}\mRightarrow{}  (\mneg{}\muparrow{}f[last(p1)]))
{}\mRightarrow{}  (\mneg{}\muparrow{}null(fst(case  p1  of  []  =>  <[],  [u  /  p2]>  |  x::y  =>  <[u  /  p1],  p2>  esac)))
{}\mRightarrow{}  (\mneg{}\muparrow{}f[last(fst(case  p1  of  []  =>  <[],  [u  /  p2]>  |  x::y  =>  <[u  /  p1],  p2>  esac))])


By

---

Latex:
(ListInd  (-3)  THEN  Reduce  0  THEN  Auto)

---

Home Index