---

Step * of Lemma accumulate_abort_wf

∀[A,B:Type]. ∀[s:B?]. ∀[F:A ⟶ B ⟶ (B?)]. ∀[L:A List].
  accumulate_abort(x,sofar.F[x;sofar];s;L) ∈ B? supposing valueall-type(B)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[s:B?].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  (B?)].  \mforall{}[L:A  List].
    accumulate\_abort(x,sofar.F[x;sofar];s;L)  \mmember{}  B?  supposing  valueall-type(B)


By

---

Latex:
ProveWfLemma

---

Home Index