tweak prim1_to_bc and prove prim1_to_bc_thm