fix some proofs in intLangExtra
add new case to prim2_to_bc_thm