---

Step * 2 1 of Lemma last-insert


1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[x:T]. (last(insert(x;v)) = if null(v) then x else last(v) fi  ∈ T)
6. x : T
⊢ last(if x ∈b <u, v> then <u, v> else [x / <u, v>] fi ) = last([u / v]) ∈ T
BY
{ (Fold `cons` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[x:T].  (last(insert(x;v))  =  if  null(v)  then  x  else  last(v)  fi  )
6.  x  :  T
\mvdash{}  last(if  x  \mmember{}\msubb{}  <u,  v>  then  <u,  v>  else  [x  /  <u,  v>]  fi  )  =  last([u  /  v])


By

---

Latex:
(Fold  `cons`  0  THEN  AutoSplit)

---

Home Index