---

Step * of Lemma bm_foldli_aux_wf

∀[T,U,Key:Type]. ∀[f:Key ⟶ T ⟶ U ⟶ U]. ∀[m:binary-map(T;Key)].  (bm_foldli_aux(f;m) ∈ U ⟶ U)
BY
{ ((Auto THEN D -1)
   THEN BinMapInd `m'
   THEN RepUR ``bm_foldli_aux`` 0
   THEN Try (Fold `bm_foldli_aux` 0)
   THEN Auto
   THEN RWO "bm_cnt_prop_T" (-2)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  D  -1)
  THEN  BinMapInd  `m'
  THEN  RepUR  ``bm\_foldli\_aux``  0
  THEN  Try  (Fold  `bm\_foldli\_aux`  0)
  THEN  Auto
  THEN  RWO  "bm\_cnt\_prop\_T"  (-2)
  THEN  Auto)

---

Home Index