---

Step * 2 2 of Lemma split_tail_rel


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

---

Latex:

---

Latex:

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


By

---

Latex:
(ListInd  (-2)  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index