fact: Definition dee_eval φ ν e := match e with | dee_nat n => n | dee_var v => φ v | dee_par i => ν i | dee_comp o v w => de_op_sem o (φ v) (φ w) end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)