proposition: Fact get_set_env_neq e v p q : p <> q -> get_env (set_env e p v) q = get_env e q.
proof: Proof. simpl; intros H; unfold set_env, get_env; destruct (X_eq_dec p q); auto; destruct H; auto. Qed.
imports: Undecidability.Shared.Libs.DLW.Utils(utils)