Strengthen bir_post_bir_to_arch

[palmskog]

I had to strengthen bir_post_bir_to_<arch> again to do the connection between arch PC and BIR PC. This is the theorem needed for the isqrt example:

Theorem riscv_bmr_bpc_label_c_PC_BST_Running:
!b f b1 ms w.
 bmr_rel riscv_bmr (bir_state_t b (BEnv f) BST_Running) ms /\
 b.bpc_label = BL_Address (Imm64 w) ==>
 ms.c_PC ms.procID = w

[didriklundberg]

This looks reasonable.