update proof of prim2_to_bc_thm

required a slight change of statement (stronger precondition)