proposition: Lemma list_sum_append l ls offset : l + (list_sum ls + offset) = list_sum (ls ++ [l]) + offset.
proof: Proof. rewrite list_sum_app /=. lia. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun