---

Step * of Lemma assert_of_mon_eq

∀[s:DMon]. ∀[a,b:|s|].  uiff(↑(a =b b);a = b ∈ |s|)
BY
{ ((UnivCD) THENA Auto) }

1
1. s : DMon
2. a : |s|
3. b : |s|
⊢ uiff(↑(a =b b);a = b ∈ |s|)

---

Latex:

---

Latex:
\mforall{}[s:DMon].  \mforall{}[a,b:|s|].    uiff(\muparrow{}(a  =\msubb{}  b);a  =  b)


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index