---

Step * 1 of Lemma last_index_append

.....equality..... 
1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
⊢ last_index(as @ bs;x.P[x]) ~ snd(accumulate (with value p and list item x):
                                    let n,lst = p 
                                    in <n + 1, if P[x] then n + 1 else lst fi >
                                   over list:
                                     bs
                                   with starting value:
                                    <||as||, last_index(as;x.P[x])>))
BY
{ xxx(Unfold `last_index` 0
      THEN (RWO "list_accum_append" 0 THENA Auto)
      THEN Fold `last_index` 0
      THEN RepeatFor 2 (EqCD)
      THEN Try (Trivial))xxx }

1
1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
⊢ accumulate (with value p and list item x):
   let n,lst = p 
   in <n + 1, if P[x] then n + 1 else lst fi >
  over list:
    as
  with starting value:
   <0, 0>) ~ <||as||, last_index(as;x.P[x])>

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  last\_index(as  @  bs;x.P[x])  \msim{}  snd(accumulate  (with  value  p  and  list  item  x):
                                                                        let  n,lst  =  p 
                                                                        in  <n  +  1,  if  P[x]  then  n  +  1  else  lst  fi  >
                                                                      over  list:
                                                                          bs
                                                                      with  starting  value:
                                                                        <||as||,  last\_index(as;x.P[x])>))


By

---

Latex:
xxx(Unfold  `last\_index`  0
        THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
        THEN  Fold  `last\_index`  0
        THEN  RepeatFor  2  (EqCD)
        THEN  Try  (Trivial))xxx

---

Home Index