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