proposition: Fact mm_sss_env_DEC0_inv x k i v j w : v⇢x = O -> DEC x k // (i,v) -1> (j,w) -> j = k /\ w = v.
proof: Proof. intros H; inversion 1; subst; auto; rewrite H in H2; try discriminate. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)