proposition: Fact mma_null_progress v st : st = (1+i,v[0/x]) -> (i,mma_null) // (i,v) -+> st.
proof: Proof. intros; subst. apply mma_null_spec with (1 := eq_refl); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)