proposition: Fact link_app i ll mm j : link i (ll++mm) j = link i ll j ++ link (length ll+i) mm (lsum ll+j).
proof: Proof. revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; f_equal. rewrite IH; do 2 f_equal; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)