proposition: Fact dee_eval_ext e φ1 ν1 φ2 ν2 : (forall x, dee_vars e x -> φ1 x = φ2 x) -> (forall x, ν1 x = ν2 x) -> dee_eval φ1 ν1 e = dee_eval φ2 ν2 e.
proof: Proof. destruct e as [ | | | [] ]; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)