---

Step * of Lemma next-unfold

∀[k,p:Top].  ((next i > k s.t. ↑p[i]) ~ eval j = k + 1 in if p[j] then j else (next i > j s.t. ↑p[i]) fi )
BY
{ ((UnivCD THENA Auto) THEN RW (AddrC [1] (RecUnfoldC `next`)) 0 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[k,p:Top].
    ((next  i  >  k  s.t.  \muparrow{}p[i])  \msim{}  eval  j  =  k  +  1  in
                                                          if  p[j]  then  j  else  (next  i  >  j  s.t.  \muparrow{}p[i])  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (AddrC  [1]  (RecUnfoldC  `next`))  0  THEN  Trivial)

---

Home Index