fact: Fixpoint dp_var_list p := match p with | dp_nat _ => nil | dp_var v => v::nil | dp_par _ => nil | dp_comp _ p q => dp_var_list p ++ dp_var_list q end.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)