Step
*
of Lemma
bm_cnt_prop_E
bm_cnt_prop(bm_E()) ~ tt
BY
{ (Reduce 0 THEN Auto) }
Latex:
bm\_cnt\_prop(bm\_E())  \msim{}  tt
By
(Reduce  0  THEN  Auto)
Home
Index