proposition: Fact mma_null_list_length l i : length (mma_null_list l i) = length l.
proof: Proof. revert i; induction l; simpl; intro; f_equal; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)