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