proposition: Fact get_set_env_eq e v p q : p = q -> get_env (set_env e p v) q = v.
proof: Proof. intros []; unfold set_env, get_env; destruct (X_eq_dec p p) as [ | [] ]; auto. Qed.
imports: Undecidability.Shared.Libs.DLW.Utils(utils)