proposition: Fact dee_vars_dec k e x : dee_vars (dee_dec k e) x -> x = k \/ dee_vars e x.
proof: Proof. destruct e as [ | | [] | [] ]; simpl; firstorder. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)