save the prim_bs_eq theorem

probably facts about prim_bs should instead be recoverable from
various invariants about it, but sometimes it's just easier to inspect
it directly. in particular what I needed to know is that adding code to
it is the same as "install_code" after it runs (i.e. the output is empty
anyway, and the pc is at the end anyway).
finish updating bootstrap lemmas