---

Step * of Lemma decidable__mon_eq

∀g:DMon. ∀a,b:|g|.  Dec(a = b ∈ |g|)
BY
{ UnivCD THENM D 1 
THENA Auto }

1
1. g : Mon@i'
2. IsEqFun(|g|;=b)
3. a : |g|@i
4. b : |g|@i
⊢ Dec(a = b ∈ |g|)

---

Latex:

---

Latex:
\mforall{}g:DMon.  \mforall{}a,b:|g|.    Dec(a  =  b)


By

---

Latex:
UnivCD  THENM  D  1 
THENA  Auto

---

Home Index