proposition: Fact linker_in_code j : in_code j P -> in_code (linker j) (i,compiler).
proof: Proof. Proof using Hc Hlc. intros H; red in H; simpl in H. destruct (@list_split_length _ (snd P) (j - fst P)) as (ll & mm & H1 & H2); try lia. replace j with (length ll+fst P) by lia. rewrite (linker_app _ _ H1). red; simpl; rewrite compiler_length, H1, length_compiler_app. rewrite H1, app_length in H. destruct mm as [ | x mm ]. + simpl in H; lia. + simpl. generalize (Hlc x); lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)