fact: Fixpoint dp_par_list p := match p with | dp_cnst _ => nil | dp_var _ => nil | dp_par x => x::nil | dp_comp _ p q => dp_par_list p ++ dp_par_list q end.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10.Dio(dio_logic dio_single) Undecidability.H10.ArithLibs(Zp lagrange)