proposition: Lemma solved_var_swapp_eq : forall x s t l sigma, is_a_solved_var x (mk_pb sigma ((s,t) :: l)) = is_a_solved_var x (mk_pb sigma ((t,s) :: l)).
proof: Proof. intros x s t l sigma; case_eq (is_a_solved_var x (mk_pb sigma ((s, t) :: l))). intro x_solved; rewrite solved_var in x_solved; symmetry; rewrite solved_var. destruct (find X.eq_bool x sigma) as [x_val | ]; trivial. destruct x_solved as [x_not_in_s_t_l x_not_in_sigma]; split; [intros x_in_t_s_l | trivial]. apply x_not_in_s_t_l; destruct_set x_in_t_s_l x_in_t_s x_in_l. destruct_set x_in_t_s x_in_t x_in_s. apply VSet.union_1; apply VSet.union_2; trivial. do 2 apply VSet.union_1; trivial. apply VSet.union_2; trivial. intro x_not_solved; rewrite not_solved_var in x_not_solved; symmetry; rewrite not_solved_var. destruct (find X.eq_bool x sigma) as [x_val | ]; trivial. destruct x_not_solved as [x_in_s_t_l | x_in_sigma]; [left | right; trivial]. destruct_set x_in_s_t_l x_in_s_t x_in_l. destruct_set x_in_s_t x_in_s x_in_t. apply VSet.union_1; apply VSet.union_2; trivial. do 2 apply VSet.union_1; trivial. apply VSet.union_2; trivial. Defined.
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)