proposition: Lemma empty_solver Pb : is_problem_empty Pb = true -> Prob_WF Pb.
proof: Proof. unfold Prob_WF; destruct Pb; simpl; intros; destruct R; try solve [termination_trivial | discr]. Qed.
imports: CoLoR(ListUtil Problem ATrs SN LogicUtil)