proposition: Fact mma_null_all_length : length mma_null_all = n.
proof: Proof. unfold mma_null_all. rewrite mma_null_list_length. apply pos_list_length. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)