---

Step * 1 of Lemma dmon_properties


1. g : DMon
⊢ IsEqFun(|g|;=b)
BY
{ (BasicAbSetHD 1 THEN Auto) }

1
1. g : Mon
2. [%1] : IsEqFun(|g|;=b)
⊢ IsEqFun(|g|;=b)

---

Latex:

---

Latex:

1.  g  :  DMon
\mvdash{}  IsEqFun(|g|;=\msubb{})


By

---

Latex:
(BasicAbSetHD  1  THEN  Auto)

---

Home Index