---

Step * of Lemma bm_min_wf

∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  bm_min(m) ∈ Key × T supposing ↑bm_T?(m)
BY
{ (Auto
   THEN BinMapInd `m'
   THEN RepUR ``bm_min`` 0
   THEN Fold `bm_min` 0
   THEN DVarSets
   THEN BinMapCase `left'
   THEN Auto
   THEN BackThruSomeHyp
   THEN Reduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m:binary\_map(T;Key)].    bm\_min(m)  \mmember{}  Key  \mtimes{}  T  supposing  \muparrow{}bm\_T?(m)


By

(Auto
  THEN  BinMapInd  `m'
  THEN  RepUR  ``bm\_min``  0
  THEN  Fold  `bm\_min`  0
  THEN  DVarSets
  THEN  BinMapCase  `left'
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Reduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index