proposition: Fact mm_sss_env_fun i s t1 t2 : i // s -1> t1 -> i // s -1> t2 -> t1 = t2.
proof: Proof. intros []; subst. inversion 1; subst; auto. inversion 1; subst; auto. rewrite H in H6; discriminate. inversion 1; subst; auto. rewrite H in H6; discriminate. rewrite H in H6; inversion H6; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)