proposition: Fact mm_sss_env_INC_inv x i v j w : INC x // (i,v) -1> (j,w) -> j=1+i /\ w = v⦃x⇠S(v⇢x)⦄.
proof: Proof. inversion 1; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)