fact: Fixpoint df_weight_1 f := match f with | df_cst _ _ => 6 | df_eq _ _ => 6 | df_op _ _ _ _ => 8 | df_bin _ f g => 1 + df_weight_1 f + df_weight_1 g | df_exst f => 1 + df_weight_1 f end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)