---

Step * 1 of Lemma list_ind_reverse_unfold


1. A : Type
2. B : Type
3. nilcase : B
4. F : B ⟶ (A List) ⟶ A ⟶ B
5. L : A List
6. ||L|| > 0
⊢ if (||L|| =z 0) then nilcase else F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L) fi  
~ F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)
BY
{ AutoSplit }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  nilcase  :  B
4.  F  :  B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B
5.  L  :  A  List
6.  ||L||  >  0
\mvdash{}  if  (||L||  =\msubz{}  0)
then  nilcase
else  F  list\_ind\_reverse(firstn(||L||  -  1;L);nilcase;F)  firstn(||L||  -  1;L)  last(L)
fi    \msim{}  F  list\_ind\_reverse(firstn(||L||  -  1;L);nilcase;F)  firstn(||L||  -  1;L)  last(L)


By

---

Latex:
AutoSplit

---

Home Index