proposition: Fact linker_err_code j : j < fst P \/ length (snd P) + fst P < j -> linker j = err.
proof: Proof. unfold linker. destruct P as (iP,lP); simpl; intros H. dest eq nat dec as [ H1 | _ ]; [ lia | ]. generalize (list_assoc_In eq_nat_dec j (link iP lP i)). destruct (list_assoc eq_nat_dec j (link iP lP i)); auto. intros H1. apply in_map with (f := @fst _ _) in H1. rewrite link_fst, list_an_spec in H1; simpl in H1; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)