---

Step * 1 of Lemma assert_of_mon_eq


1. s : DMon
2. a : |s|
3. b : |s|
⊢ uiff(↑(a =b b);a = b ∈ |s|)
BY
{ (AddProperties 1     THEN UnfoldTopAb 2   THEN Sel (-1) (BHyp 2) THEN Auto ) }

---

Latex:

---

Latex:

1.  s  :  DMon
2.  a  :  |s|
3.  b  :  |s|
\mvdash{}  uiff(\muparrow{}(a  =\msubb{}  b);a  =  b)


By

---

Latex:
(AddProperties  1          THEN  UnfoldTopAb  2      THEN  Sel  (-1)  (BHyp  2)  THEN  Auto  )

---

Home Index