---

Step * of Lemma bm_foldli_wf

∀[T,U,Key:Type]. ∀[f:Key ⟶ T ⟶ U ⟶ U]. ∀[m:binary-map(T;Key)]. ∀[init:U].  (bm_foldli(f;init;m) ∈ U)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T,U,Key:Type].  \mforall{}[f:Key  {}\mrightarrow{}  T  {}\mrightarrow{}  U  {}\mrightarrow{}  U].  \mforall{}[m:binary-map(T;Key)].  \mforall{}[init:U].
    (bm\_foldli(f;init;m)  \mmember{}  U)


By

---

Latex:
ProveWfLemma

---

Home Index