proposition: Lemma Dummy_bool : forall b, negb b = true <-> b = false.
proof: Proof. intros [ | ]; intuition. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)