---

Step * of Lemma bor_mon_wf

<𝔹,∨b> ∈ AbMon
BY
{ (Unfold `bor_mon` 0 
   THEN ((BLemma `mk_abmonoid`) THENA Auto)
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN AutoBoolCase ⌜x⌝⋅
   THEN AutoBoolCase ⌜y⌝⋅) }

---

Latex:

---

Latex:
<\mBbbB{},\mvee{}\msubb{}>  \mmember{}  AbMon


By

---

Latex:
(Unfold  `bor\_mon`  0 
  THEN  ((BLemma  `mk\_abmonoid`)  THENA  Auto)
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoBoolCase  \mkleeneopen{}x\mkleeneclose{}\mcdot{}
  THEN  AutoBoolCase  \mkleeneopen{}y\mkleeneclose{}\mcdot{})

---

Home Index