fact: Definition dee_vars e x := match e with | dee_nat _ => False | dee_var v => x = v | dee_par _ => False | dee_comp _ v w => x = v \/ x = w end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)