Step 
*
 of Lemma 
bm_cnt_prop_E_reduce_lemma
bm_cnt_prop(bm_E()) ~ tt
BY
 
{ (UnivCD THENA Auto) }
1
bm_cnt_prop(bm_E()) ~ tt
 
Latex: 
Latex:
bm\_cnt\_prop(bm\_E())  \msim{}  tt
 By 
Latex:
(UnivCD  THENA  Auto)
Home
Index