fact: Definition linker := let ll := (length (snd P) + fst P,lsum (snd P)+i)::link (fst P) (snd P) i in fun j => match list_assoc eq_nat_dec j ll with | None => err | Some p => p end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)