---

Step * of Lemma list_ind-as-fix

∀[L:Top List]. ∀[x,F:Top].
  (rec-case(L) of
   [] => x
   b::bs =>
    r.F[r;b;bs] ~ fix((λR,L. if null(L) then x else F (R tl(L)) hd(L) tl(L) fi )) L)
BY
{ (Unfold `so_apply` 0
   THEN InductionOnList
   THEN Auto
   THEN (Reduce 0
         THEN RW (AddrC [2] UnrollRecursionC) 0
         THEN Reduce 0
         THEN RepeatFor 3 (EqCD)
         THEN Auto
         THEN BackThruSomeHyp)⋅) }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[x,F:Top].
    (rec-case(L)  of
      []  =>  x
      b::bs  =>
        r.F[r;b;bs]  \msim{}  fix((\mlambda{}R,L.  if  null(L)  then  x  else  F  (R  tl(L))  hd(L)  tl(L)  fi  ))  L)


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  InductionOnList
  THEN  Auto
  THEN  (Reduce  0
              THEN  RW  (AddrC  [2]  UnrollRecursionC)  0
              THEN  Reduce  0
              THEN  RepeatFor  3  (EqCD)
              THEN  Auto
              THEN  BackThruSomeHyp)\mcdot{})

---

Home Index