proposition: Fact mm_nullify_length i lr : length (mm_nullify i lr) = 2*length lr.
proof: Proof. revert i; induction lr as [ | x lr IH ]; simpl; intros i; auto. rewrite IH; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)