proposition: Fact linker_code_end : linker (code_end P) = lsum (snd P)+i.
proof: Proof. unfold code_end; rewrite Nat.add_comm. apply (linker_app _ nil), eq_sym, app_nil_r. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)