proposition: Lemma VSet_compat : forall pb (e e' : DecVar.A), DecVar.eq_A e e' -> (fun v : variable => negb (is_a_solved_var v pb)) e = (fun v : variable => negb (is_a_solved_var v pb)) e'.
proof: Proof. unfold VSet.EDS.eq_A, DecVar.eq_A. intros; subst; split; intro; assumption. 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)