proposition: Fact linker_app ll mm : snd P = ll++mm -> linker (length ll+fst P) = lsum ll + i.
proof: Proof. intros H; unfold linker. destruct P as (iP,lP). rewrite H; simpl in H |- *. destruct mm as [ | x mm ]. * rewrite app_nil_r. solve eq nat dec. * rew length. dest eq nat dec as [ H1 | H1 ]; [ lia | clear H1 ]. rewrite link_app, list_assoc_app. generalize (list_assoc_In eq_nat_dec (length ll + iP) (link iP ll i)). destruct (list_assoc eq_nat_dec (length ll + iP) (link iP ll i)) as [ j | ]. - intros H1. apply in_map with (f := @fst _ _) in H1. rewrite link_fst, list_an_spec in H1; simpl in H1; lia. - intros; simpl; solve eq nat dec. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)