proposition: Fact linker_out_code j : err < i \/ length_compiler (snd P) + i <= err -> out_code j P -> out_code (linker j) (i,compiler).
proof: Proof. Proof using Hc. intros H1 H2. red in H2. destruct (eq_nat_dec j (code_end P)) as [ H | H ]. rewrite H, linker_code_end; simpl. rewrite compiler_length; lia. rewrite linker_err_code. simpl; rewrite compiler_length; lia. simpl in H2, H; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)